Equivalence of category of subsets and subobjects I'm trying to show that the categories $\mathcal{P}(X)$ and $Sub(X)$ are equivalent.
According to Steve Awodey's "Category Theory" I need to find two functors


*

*$ E: \mathcal{P}(X) \to Sub(X)$

*$F: Sub(X) \to \mathcal{P}(X)$


and a pair of natural isomorphisms


*

*$\alpha: 1_{\mathcal{P}(X)} \overset{\sim}{\to} F \circ E$  

*$\beta: 1_{Sub(X)}: \overset{\sim}{\to} E \circ F$


I believe I've constructed E and F correctly on the objects. On object $Y \in \mathcal{P}(X)$ I define $E(Y) = \lambda y. y$, and since $Y$ is a subset of $X$ this has the type $Y \to X$ as required.
On object $f \in Sub(X)$ I define $E(f) = \lbrace f(x) \mid x \in \mathsf{dom}(f) \rbrace \subseteq X$ as required.
I'm not sure how I define the functors on morphisms in both cases though.
Edit: I forgot to define $Sub(X)$, so here's a definition:
The objects in $Sub(X)$ are monomorphisms $m$ with $cod(m) = X$ and the given two objects $m$ and $m'$ an arrow in $Sub(X)$ is $f: m \to m'$ such that $m = m' \circ f$.
Hopefully that clears things up.

Well, what are the arrows in $P(X)$?  
I assume it is the poset category, ie. the arrows are just the inclusions $Y_1\subseteq Y_2$.
Basically $E$ is the identity, also on arrows: for $Y_1\subseteq Y_2\subseteq X$, $\ E$ maps it to the identical inclusions $Y_1\hookrightarrow Y_2\hookrightarrow X$.
On the other hand, for an $f:m\to m'$, i.e. $m=m'\circ f$, first prove that $f$ is also a monomorphism, then take its image and map all these into $X$ by $m'$.
