Type Theories, Toposes and Constructive Set Theory: Predicative Aspects of AST
Article
Formal Antecedent
Category Theory
Citation
Ieke Moerdijk and Erik Palmgren. (2002). Type Theories, Toposes and Constructive Set Theory: Predicative Aspects of AST. Annals of Pure and Applied Logic. 114(1–3). pp. 155–201.
Why this reference is included
Moerdijk and Palmgren’s 2002 Type Theories, Toposes and Constructive Set Theory: Predicative Aspects of AST, published in Annals of Pure and Applied Logic, is one of the program’s working technical references. Cited across Book I (Categorical Foundations), Part 18, Chapter The Self-Hosting Landscape; Book I (Categorical Foundations), Part 18, Chapter The Enrichment Frontier — the central framing is “Moerdijk and Palmgren developed the theory of predicative toposes — specifically, Π W-pretoposes as a predicative analogue of elementary toposes”.
Cited in
-
Book I — Categorical Foundations Part 18Chapter The Self-Hosting Landscape
Moerdijk and Palmgren developed the theory of predicative toposes — specifically, Π W-pretoposes as a predicative analogue of elementary toposes
-
Book I — Categorical Foundations Part 18Chapter The Enrichment Frontier
Moerdijk and Palmgren construct predicative toposes that model dependent type theory without assuming classical logic
-
Book I — Categorical Foundations Part 18Chapter The Enrichment Frontier
The enrichment frontier classification assigns a novelty status to each transition of the enrichment ladder: E_0 → E_1: Achieved. Internalizing types within a categorical framework has been accomplished by multiple groups (Altenkirch–Kaposi , Bocquet–Kaposi–Sattler , Moerdijk–Palmgren )