# 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 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 \autorefsec:piw-pretopos roughly follows that in [RijkeSpitters].
The fact that epimorphisms^{} are surjective^{} (\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 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^{} ${\mathcal{U}}_{i}$ is surjective if it is an epimorphism in the next universe ${\mathcal{U}}_{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 \autorefthm:1surj_to_surj_to_pem from $\mathrm{\U0001d5a0\U0001d5a2}$ to $\mathrm{\U0001d5ab\U0001d5a4\U0001d5ac}$ 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 \autorefsec:cumulative-hierarchy of the cumulative hierarchy, is due to [JoyalMoerdijk1995], but it derives from earlier work by [AczelCZF].

Title | Chapter 10 Notes |
---|---|

\metatable |