OK, I did.

]]>Right, it should say “simply choose one object in each isomorphism class and one isomorphism to that object from each other object in that class” (or something like that).

]]>Entry skeleton says: “If the axiom of choice holds, then every category has a skeleton: simply choose one object in each isomorphism class.”

When the construction *is* simple, the proof is a tiny bit more subtle, namely one has to show that the inclusion $in:sk(C)\to C$ is really an equivalence. For the weak inverse one forms a functor
$-':x\mapsto x'$ as follows. For every object $x$ one has chosen already the unique object $x'$ in $sk(X)$ isomorphic to $x$, but one also needs to make *a choice of isomorphism* $i_x:x\to x'$ for every $x$. This enables to conjugate between $C(x,y)$ and $C(x',y')$ by

This correspondence makes $-'$ a functor, that is the rule for morphisms $f' := i_y\circ f\circ i_{x}^{-1}$ is functorial. Let us show that $-'$ is a weak inverse of $in$. In one direction, $(in_{y})' = y$ for $y\in sk(C)$; in another direction notice that $i^{-1}_{in_{x'}}:in_{x'}\cong x$ for $x\in C$ is an isomorphism. It suffices to show that these isomorphisms form a *natural* isomorphism $i^{-1}_{in}:in_{-'}\to id_C$; the naturality diagram is commutative precisely because of the conjugation formula for the functor $-'$ for morphisms.

Right ?

]]>Added a bit to skeleton about skeletons of internal categories

]]>