10.1.4 Set is a $\mathrm{\Pi }𝖶$-pretopos

The notion of a $\mathrm{\Pi }\mathit{}\mathrm{W}$-pretopos— that is, a locally cartesian closed categorywith disjoint finite coproducts, effective equivalence relations, and initial algebras for polynomial endofunctors — is intended as a “predicative”notion of topos, i.e. a category of “predicative sets”, which can serve the purpose for constructive mathematicsthat the usual category of sets does for classicalmathematics.

Typically, in constructive type theory, one resorts to an external construction of “setoids” — an exact completion — to obtain a category with such closure properties.In particular, the well-behaved quotients are required for many constructions in mathematics that usually involve (non-constructive) power sets. It is noteworthy that univalent foundations provides these constructions internally (via higher inductive types), without requiring such external constructions. This represents a powerful advantage of our approach, as we shall see in subsequent examples.

Theorem 10.1.1.

The category $\mathrm{S}\mathit{}e\mathit{}t$ is a $\mathrm{\Pi }\mathit{}\mathrm{W}$-pretopos.

Proof.

We have an initial object$\mathrm{𝟎}$ and finite, disjoint sums $A+B$. These are stable under pullback, simply because pullback has a right adjoint. Indeed, $𝒮et$ is locally cartesian closed, since for any map $f:A\to B$ between sets, the “fibrant replacement” ${\sum }_{(a:A)}f(a)=b$ is equivalent to $A$ (over $B$), and we have dependent function types for the replacement.We’ve just shown that $𝒮et$ is regular (thm:set_regular) and that quotients are effective (lem:sets_exact). We thus have a locally cartesian closed pretopos. Finally, since the $n$-types are closed under the formation of $W$-types by ex:ntypes-closed-under-wtypes, and by thm:w-hinit $W$-types are initial algebras for polynomial endofunctors, we see that $𝒮et$ is a $\mathrm{\Pi }𝖶$-pretopos.∎

One naturally wonders what, if anything, prevents $𝒮et$ from being an (elementary) topos?In addition to the structure already mentioned, a topos has asubobject classifier:a pointed object classifying (equivalence classes of) monomorphisms. (In fact, in the presence of a subobjectclassifier, things become somewhat simpler: one merely needs cartesian closure in order to get the colimits.)In homotopy type theory, univalence implies that the type $\mathrm{𝖯𝗋𝗈𝗉}:\equiv {\sum }_{(X:𝒰)}\mathrm{𝗂𝗌𝖯𝗋𝗈𝗉}(X)$ does classify monomorphisms (by an argument similar to sec:object-classification), but in general it is as large as the ambient universe $𝒰$.Thus, it is a “set” in the sense of being a $0$-type, but it is not “small” in the sense of being an object of $𝒰$, hence not an object of the category $𝒮et$.However, if we assume an appropriate form of propositional resizing (see subsec:prop-subsets), then we can find a small version of $\mathrm{𝖯𝗋𝗈𝗉}$, so that $𝒮et$ becomes an elementary topos.

Theorem 10.1.2.

If there is a type $\mathrm{\Omega }\mathrm{:}\mathrm{U}$ of all mere propositions, then the category $\mathrm{S}\mathit{}e\mathit{}{t}_{\mathrm{U}}$ is an elementary topos.

A sufficient condition for this is the law of excluded middle, in the “mere-propositional” form that we have called $\mathrm{𝖫𝖤𝖬}$; for then we have $\mathrm{𝖯𝗋𝗈𝗉}=\mathrm{𝟐}$, which is small, and which then also classifies all mere propositions.Moreover, in topos theory a well-known sufficient condition for $\mathrm{𝖫𝖤𝖬}$ is the axiom of choice, which is of course often assumed as an axiom in classical set theory.In the next section, we briefly investigate the relation between these conditions in our setting.