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 $\\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 $\\mathsf{AC}$ to $\\mathsf{LEM}$ is an adaptation to homotopy typetheory 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].

单词	Chapter10Notes
释义	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 $\\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 $\\mathsf{AC}$ to $\\mathsf{LEM}$ is an adaptation to homotopy typetheory 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].
随便看	fix (transformation action) Flag flag FlagVariety flag variety FlatModule flat module FlatMorphism flat morphism FlatResolution flat resolution FleurysAlgorithm Fleury’s algorithm FlexibleAlgebra flexible algebra Flow flow flow Flow1 FloydsAlgorithm Floyd’s algorithm FluxOfVectorField flux of vector field FodorsLemma Fodor’s lemma