# 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.

• You'll have to be more specific - it is not clear how $\mathcal{Sub}(X)$ is defined differently from $\mathcal{P}(X)$. – Thomas Andrews Apr 27 '15 at 21:25
• Oh sorry. I've added a definition in an edit now – Michael Apr 27 '15 at 21:30
• I think you can work less. If you prove that one of your functors is full, faithfull and essentially surjective on objects you're done. – Abellan Apr 27 '15 at 21:50

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'$.