Skeleton of a category (source code)

= Skeleton of a category

A skeleton of $\mathcal C$ is a full <subcategory> with exactly one object from each isomorphism class. The <axiom of choice> supplies skeletons of <small categories>. Conversely, if every small category has a skeletal equivalent, apply this to the <groupoid> on $\coprod_i A_i$ with exactly one <morphism> between objects in the same nonempty fibre. A quasi-inverse from the skeletal category selects one object per fibre, giving a choice function. This converse uses an <equivalence of categories> with specified quasi-inverse functors, not just the existence of a full essentially surjective functor in one direction.