Developing category theory inside ETCS

Solution 1:

The point of ETCS is that a model of ETCS is already a category, so I suppose what you are asking for is how to do universes in ETCS. Well, ETCS is equivalent in a strong sense to Mac Lane set theory, and in Mac Lane set theory, Grothendieck universes are models of (second-order!) ZFC. So if you're willing to go down that route it suffices to axiomatise strongly inaccessible cardinals within ETCS – and this is straightforward.

Now suppose $X$ is a set of strongly inaccessible cardinality. We construct within ETCS a category of small sets based on $X$. First, let $O$ be the subset of $\mathscr{P}(X)$ consisting of those subsets of $X$ strictly smaller than $X$, and let $E \subseteq X \times O$ be the binary relation obtained by restricting $[\in]_X \subseteq X \times \mathscr{P}(X)$. We may regard the projection $E \to O$ as an $O$-indexed family of sets, and we may then form $F \to O \times O$ such that the fibre of $F$ over an element $(Y, Z)$ of $O$ is the set $Z^Y$. This has the expected universal property in the slice category $\mathbf{Set}_{/ O \times O}$. Once we have $F \to O \times O$, it is a straightforward matter to build an internal category which, when externalised, is the full subcategory of $\mathbf{Set}$ spanned by the small subsets of $X$. Note that the assumption that the cardinality of $X$ is a regular cardinal implies that the resulting category is a model of not just ETCS but also the axiom of replacement.

Of course, if one really believes ETCS is an adequate foundation for mathematics, then one can also make do with less. For instance, the same construction could be carried out for a set whose cardinality is a strong limit, and the resulting internal category of sets will still be a model of ETCS though not necessarily of replacement.

Solution 2:

First, note that the theory of categories is one-sorted in nature, despite it is usually presented as two-sorted (objects, arrows), since you can identify an object with its identity arrow.

The ETCS is actually part of a larger formal system, the Elementary Theory of the Category of Categories [ETCC], where alphabet's variables represent morphisms between categories. The most important objects, that have to be axiomatized, are the categories $\mathbf{0, 1, 2, 3}$. A good reference may be: Elementary Categories, Elementary Toposes.

Lawvere, in his beautiful PhD thesis, suggested to deal with dimensional problems in a way very similar to ZF3 (i.e., ZF enhanced with universes $\omega = \theta_0 \in \theta_1\in \theta_2$). Thus, he proposed to axiomatize the existence of two categories (i.e., variables)

• $\mathcal C_1$ which has to be thought of as the category of small categories. Here, the most important category of sets is $\mathbf{FinSet}$ (Bill calls it $\mathcal S_0$). One requires it to have all the nice properties of $\mathbf{Cat}$.
• $\mathcal C_2$ which has to be thought of as the category of large categories. One requires it has all the nice properties of $\mathcal C_1$ and moreover an identity arrow (i.e., an object, a category) with all its properties (that is, $\mathcal C_1$). Of course, the category of small sets may be considered as an object of $\mathcal C_2$, i.e., an arrow $\{\mathcal S_1\}\colon \mathbf 1 \to \mathcal C_2$.

In this general framework, one can axiomatize ETCS.

Also, take a look to these 3d on MO: 1, 2.