# 10.1.4 Set is a $\Pi\mathsf{W}$-pretopos

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 $\mathcal{S}et$ is a $\Pi\mathsf{W}$-pretopos.

###### Proof.

We have an initial object  $\mathbf{0}$ and finite, disjoint sums $A+B$. These are stable under pullback  , simply because pullback has a right adjoint. Indeed, $\mathcal{S}et$ is locally cartesian closed, since for any map $f:A\to B$ between sets, the “fibrant replacement” $\mathchoice{\sum_{a:A}\,}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a:A)}}{% \sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a:A)% }}{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a% :A)}}{\sum_{(a:A)}}{\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 $\mathcal{S}et$ is regular  (\autorefthm:set_regular) and that quotients are effective (\autoreflem:sets_exact). We thus have a locally cartesian closed pretopos. Finally, since the $n$-types are closed under the formation of $W$-types by \autorefex:ntypes-closed-under-wtypes, and by \autorefthm:w-hinit $W$-types are initial algebras for polynomial endofunctors, we see that $\mathcal{S}et$ is a $\Pi\mathsf{W}$-pretopos. ∎

One naturally wonders what, if anything, prevents $\mathcal{S}et$ from being an (elementary) topos? In addition to the structure  already mentioned, a topos has a subobject classifier: a pointed object classifying (equivalence classes  of) monomorphisms        . (In fact, in the presence of a subobject classifier, things become somewhat simpler: one merely needs cartesian closure in order to get the colimits  .) In homotopy type theory, univalence implies that the type $\mathsf{Prop}:\!\!\equiv\mathchoice{\sum_{X:\mathcal{U}}\,}{\mathchoice{{% \textstyle\sum_{(X:\mathcal{U})}}}{\sum_{(X:\mathcal{U})}}{\sum_{(X:\mathcal{U% })}}{\sum_{(X:\mathcal{U})}}}{\mathchoice{{\textstyle\sum_{(X:\mathcal{U})}}}{% \sum_{(X:\mathcal{U})}}{\sum_{(X:\mathcal{U})}}{\sum_{(X:\mathcal{U})}}}{% \mathchoice{{\textstyle\sum_{(X:\mathcal{U})}}}{\sum_{(X:\mathcal{U})}}{\sum_{% (X:\mathcal{U})}}{\sum_{(X:\mathcal{U})}}}\mathsf{isProp}(X)$ does classify monomorphisms (by an argument  similar to \autorefsec:object-classification), but in general it is as large as the ambient universe  $\mathcal{U}$. 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 $\mathcal{U}$, hence not an object of the category $\mathcal{S}et$. However, if we assume an appropriate form of propositional resizing (see \autorefsubsec:prop-subsets), then we can find a small version of $\mathsf{Prop}$, so that $\mathcal{S}et$ becomes an elementary topos.

###### Theorem 10.1.2.

If there is a type $\Omega:\mathcal{U}$ of all mere propositions, then the category $\mathcal{S}et_{\mathcal{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 $\mathsf{LEM}$; for then we have $\mathsf{Prop}=\mathbf{2}$, which is small, and which then also classifies all mere propositions. Moreover, in topos theory a well-known sufficient condition for $\mathsf{LEM}$ 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.

 Title 10.1.4 Set is a $\Pi\mathsf{W}$-pretopos \metatable