10.1.4 Set is a -pretopos
The notion of a -pretopos — that is, a locally cartesian closed category with 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 mathematics that the usual category of sets does for classical mathematics.
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.
The category is a -pretopos.
We have an initial object and finite, disjoint sums . These are stable under pullback, simply because pullback has a right adjoint. Indeed, is locally cartesian closed, since for any map between sets, the “fibrant replacement” is equivalent to (over ), and we have dependent function types for the replacement. We’ve just shown that is regular (\autorefthm:set_regular) and that quotients are effective (\autoreflem:sets_exact). We thus have a locally cartesian closed pretopos. Finally, since the -types are closed under the formation of -types by \autorefex:ntypes-closed-under-wtypes, and by \autorefthm:w-hinit -types are initial algebras for polynomial endofunctors, we see that is a -pretopos. ∎
One naturally wonders what, if anything, prevents 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 does classify monomorphisms (by an argument similar to \autorefsec:object-classification), but in general it is as large as the ambient universe . Thus, it is a “set” in the sense of being a -type, but it is not “small” in the sense of being an object of , hence not an object of the category . However, if we assume an appropriate form of propositional resizing (see \autorefsubsec:prop-subsets), then we can find a small version of , so that becomes an elementary topos.
If there is a type of all mere propositions, then the category is an elementary topos.
A sufficient condition for this is the law of excluded middle, in the “mere-propositional” form that we have called ; for then we have , which is small, and which then also classifies all mere propositions. Moreover, in topos theory a well-known sufficient condition for 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 -pretopos|