The Clowder Project

Let $\mathcal{C}$ be a category.

1. Existence. Assuming the axiom of choice, $\mathsf{Sk}\webleft (\mathcal{C}\webright )$ always exists.
2. Pseudofunctoriality. The assignment $\mathcal{C}\mapsto \mathsf{Sk}\webleft (\mathcal{C}\webright )$ defines a pseudofunctor
   \[ \mathsf{Sk}\colon \mathsf{Cats}_{\mathsf{2}}\to \mathsf{Cats}_{\mathsf{2}}. \]
3. Uniqueness Up to Equivalence. Any two skeletons of $\mathcal{C}$ are equivalent.
4. Inclusions of Skeletons Are Equivalences. The inclusion
   \[ \iota _{\mathcal{C}}\colon \mathsf{Sk}\webleft (\mathcal{C}\webright )\hookrightarrow \mathcal{C} \]

   of a skeleton of $\mathcal{C}$ into $\mathcal{C}$ is an equivalence of categories.