10.1.4 Set is a Π⁢𝖶-pretopos


The notion of a Π⁢W-pretopos — that is, a locally cartesian closed category with disjoint finite coproductsMathworldPlanetmath, effective equivalence relations, and initial algebras for polynomialMathworldPlanetmathPlanetmathPlanetmath endofunctors — is intended as a “predicative” notion of topos, i.e. a categoryMathworldPlanetmath 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 quotientsPlanetmathPlanetmath are required for many constructions in mathematics that usually involve (non-constructive) power setsMathworldPlanetmath. 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 S⁢e⁢t is a Π⁢W-pretopos.

Proof.

We have an initial objectMathworldPlanetmath 𝟎 and finite, disjoint sums A+B. These are stable under pullbackPlanetmathPlanetmath, simply because pullback has a right adjoint. Indeed, 𝒮⁢e⁢t is locally cartesian closed, since for any map f:A→B between sets, the “fibrant replacement” ∑(a:A)f⁢(a)=b is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to A (over B), and we have dependent function types for the replacement. We’ve just shown that 𝒮⁢e⁢t is regularPlanetmathPlanetmath (\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 𝒮⁢e⁢t is a Π⁢𝖶-pretopos. ∎

One naturally wonders what, if anything, prevents 𝒮⁢e⁢t from being an (elementary) topos? In addition to the structureMathworldPlanetmath already mentioned, a topos has a subobject classifier: a pointed object classifying (equivalence classesMathworldPlanetmath of) monomorphismsMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath. (In fact, in the presence of a subobject classifier, things become somewhat simpler: one merely needs cartesian closure in order to get the colimitsMathworldPlanetmath.) In homotopy type theory, univalence implies that the type 𝖯𝗋𝗈𝗉:≡∑(X:𝒰)𝗂𝗌𝖯𝗋𝗈𝗉(X) does classify monomorphisms (by an argumentPlanetmathPlanetmath similar to \autorefsec:object-classification), but in general it is as large as the ambient universePlanetmathPlanetmath 𝒰. 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 𝒮⁢e⁢t. However, if we assume an appropriate form of propositional resizing (see \autorefsubsec:prop-subsets), then we can find a small version of 𝖯𝗋𝗈𝗉, so that 𝒮⁢e⁢t becomes an elementary topos.

Theorem 10.1.2.

If there is a type Ω:U of all mere propositions, then the category S⁢e⁢tU is an elementary topos.

A sufficient condition for this is the law of excluded middleMathworldPlanetmathPlanetmath, 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 choiceMathworldPlanetmath, which is of course often assumed as an axiom in classical set theoryMathworldPlanetmath. In the next sectionPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath, we briefly investigate the relationMathworldPlanetmathPlanetmathPlanetmath between these conditions in our setting.

Title 10.1.4 Set is a Π⁢𝖶-pretopos
\metatable