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 subsec:emacinsets was introduced by Lawvere in [lawvere:etcs-long], as a category-theoretic axiomatization of set theory. The notion of $\mathrm{\Pi }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 sec:piw-pretopos roughly follows that in [RijkeSpitters]. The fact that epimorphisms are surjective (epis-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 set operation (which is impredicative), although it can also be seen as a predicative proof of the weaker statement that a map in a universe ${𝒰}_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 implication in thm:1surj_to_surj_to_pem from $\mathrm{𝖠𝖢}$ to $\mathrm{𝖫𝖤𝖬}$ 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 numbers, see [taylor:ordinals] and also [JoyalMoerdijk1995]. Definitions of well-foundedness in type theory by an induction principle, including the inductive predicate 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 sec:cumulative-hierarchy of the cumulative hierarchy, is due to [JoyalMoerdijk1995], but it derives from earlier work by [AczelCZF].

Title	Chapter 10 Notes