Chapter 10 Notes

The basic properties one expects of the category of sets date back to the early days of elementary topos theory. The Elementary theory of the category of sets referred to in \autorefsubsec:emacinsets was introduced by Lawvere in [lawvere:etcs-long], as a category-theoretic axiomatization of set theoryMathworldPlanetmath. The notion of ΠW-pretopos, regarded as a predicative version of an elementary topos, was introduced in [MoerdijkPalmgren2002]; see also [palmgren:cetcs].

The treatment of the category of sets in \autorefsec:piw-pretopos roughly follows that in [RijkeSpitters]. The fact that epimorphismsMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath are surjectivePlanetmathPlanetmath (\autorefepis-surj) is well known in classical mathematics, but is not as trivial as it may seem to prove predicatively. The proof in [Mines/R/R:1988] uses the power setMathworldPlanetmath operationMathworldPlanetmath (which is impredicative), although it can also be seen as a predicative proof of the weaker statement that a map in a universePlanetmathPlanetmath 𝒰i is surjective if it is an epimorphism in the next universe 𝒰i+1. A predicative proof for setoids was given by Wilander [Wilander2010]. Our proof is similar to Wilander’s, but avoids setoids by using pushouts and univalence.

The implicationMathworldPlanetmath in \autorefthm:1surj_to_surj_to_pem from 𝖠𝖢 to 𝖫𝖤𝖬 is an adaptation to homotopy type theory of a theorem from topos theory due to Diaconescu [Diaconescu]; it was posed as a problem already by Bishop [Bishop1967, Problem 2].

For the intuitionistic theory of ordinal numbersMathworldPlanetmath, see [taylor:ordinals] and also [JoyalMoerdijk1995]. Definitions of well-foundedness in type theoryPlanetmathPlanetmath by an inductionMathworldPlanetmath principle, including the inductive predicateMathworldPlanetmath of accessibility, were studied in [Huet80, Paulson86, Nordstrom88], although the idea dates back to Getzen’s proof of the consistency of arithmetic [Gentzen36].

The idea of algebraic set theory, which informs our development in \autorefsec:cumulative-hierarchy of the cumulative hierarchy, is due to [JoyalMoerdijk1995], but it derives from earlier work by [AczelCZF].

Title Chapter 10 Notes