10. Set theory

Our conception of sets as types with particularly simple homotopical character, cf. sec:basics-sets, is quite different from the sets of Zermelo–Fraenkel set theory, which form acumulative hierarchy with an intricate nested membership structure.For many mathematical purposes, the homotopy-theoretic sets are just as good asthe Zermelo–Fraenkel ones, but there are important differences.

We begin this chapter in sec:piw-pretopos by showing that the category $𝒮et$ has (most of) the usual properties of the category of sets.In constructive, predicative, univalent foundations, it is a “$\mathrm{\Pi }𝖶$-pretopos”; whereas if we assume propositional resizing(subsec:prop-subsets) it is an elementary topos, and if we assume $\mathrm{𝖫𝖤𝖬}$ and $\mathrm{𝖠𝖢}$ then it is a model of Lawvere’s Elementary Theory of the Category of Sets.This is sufficient to ensure that the sets in homotopy type theory behave like sets as used by most mathematicians outside of set theory.

In the rest of the chapter, we investigate some subjects that traditionally belong to “set theory”.In sec:cardinals,sec:ordinals,sec:wellorderings we study cardinal and ordinal numbers.These are traditionally defined in set theory using the global membership relation, but we will see that the univalence axiom enables an equally convenient, more “structural” approach.

Finally, in sec:cumulative-hierarchy we consider the possibility of constructing inside of homotopy type theory a cumulative hierarchy of sets, equipped with a binary membership relation akin to that of Zermelo–Fraenkel set theory.This combines higher inductive types with ideas from the field of algebraic set theory.

In this chapter we will often use the traditional logical notation described in subsec:prop-trunc.In addition to the basic theory of cha:basics,cha:logic, we use higher inductive types for colimits and quotients as in sec:colimits,sec:set-quotients, as well as some of the theory of truncation from cha:hlevels, particularly the factorization system of sec:image-factorization in the case $n=-1$.In sec:ordinals we use an inductive family (sec:generalizations) to describe well-foundedness, and in sec:cumulative-hierarchy we use a more complicated higher inductive type to present the cumulative hierarchy.