Are (set) inclusion maps categorically definable? I have heard people say that you can "recover" the standard set theory (in terms of the ZF-constructible universe) from the category Set. I understand that the empty set is uniquely identifiable since it is initial, and that all of the singletons are identifiable (up to isomorphism) since they are final. But, it always seemed weird to me because it's hard to look "inside" of sets when you're working with Set, so I thought about trying to define the inclusion maps $f: X \to Y$ given by $f(x) = x$ in the language of category theory, but I'm having some trouble. Is it actually possible to describe these arrows (via some universal property or something), or are they inherently indistinguishable from monomorphisms in Set?
If they could be described in the categorical language, then I do think you could recover the constructible universe, because you could start from the singletons and start composing inclusions to make claims about elementhood.
 A: No, category theory is by design incapable of distinguishing isomorphic objects, and in $\text{Set}$ isomorphic sets are just sets which are in bijection with each other; this loses all of the fine detail about elements and elements of elements, etc. and this is again by design.
This is also actually consistent with mathematical practice; for example, strictly speaking it is not true that $\mathbb{N}$ is literally a subset of $\mathbb{Z}$ or that $\mathbb{Z}$ is literally a subset of $\mathbb{Q}$ or that $\mathbb{Q}$ is literally a subset of $\mathbb{R}$ or that $\mathbb{R}$ is literally a subset of $\mathbb{C}$. However, we all behave as if all of those things are true, and that's because we've fixed a particular sequence of monomorphisms $\mathbb{N} \hookrightarrow \mathbb{Z} \hookrightarrow \mathbb{Q} \hookrightarrow \mathbb{R} \hookrightarrow \mathbb{C}$ that we care about. Monomorphisms are actually the important concept in practice and category theory lets us focus on that without worrying about irrelevant "implementation details" of how sets are constructed.
Thinking about set theory from the perspective of $\text{Set}$ is structural set theory, rather than the more traditional material set theory. You can see a more detailed discussion in, for example, Leinster's Rethinking Set Theory.
A: If you are not convinced by heuristics, then here is a simple proof that subset inclusion is not a "category-theoretic" concept.
Suppose, for a contradiction, that subset inclusion is a "category-theoretic" concept.
Then it would be invariant under automorphisms of categories, i.e. for any automorphism $F : \textbf{Set} \to \textbf{Set}$ and any map $i : X \to Y$, $F i : F X \to F Y$ is a subset inclusion if and only if $i : X \to Y$ is a subset inclusion.
But we can easily construct an automorphism $F : \textbf{Set} \to \textbf{Set}$ that exchanges the objects $\{ 0 \}$ and $\{ 1 \}$ and leaves all other objects alone, doing the obvious thing for morphisms.
Clearly, such an automorphism will not preserve the inclusion $\{ 0 \} \hookrightarrow \{ 0, 1 \}$.
Therefore subset inclusion is not "category-theoretic".
What is instead true is that given $\textbf{Set}$, you can build a cumulative hierarchy of sets.
(You keep using the term "constructible universe", but I do not think it means what you think it means.)
The idea is to represent a set not as a bag of indistinguishable points but rather as a diagram encoding its elements, the elements of its elements, the elements of the elements of its elements, and so on.
If you start with a model of ZFC then you will get back an isomorphic model, but in general you may get something different.
