Type theories, toposes and constructive set theory: Predicative aspects of AST

DOI10.1016/S0168-0072(01)00079-3zbMath0999.03061OpenAlexW2121213425MaRDI QIDQ5957856

Erik Palmgren, Ieke Moerdijk

Publication date: 3 December 2002

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0168-0072(01)00079-3

zbMATH Keywords

constructive type theorysheavesAczél-Myhill set theorycategorical logicpredicative type theorystratified pseudotopostopos theory

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Topoi (18B25) Nonclassical and second-order set theories (03E70) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50)

Related Items (28)

The challenge of computer mathematics ⋮ Dependent products and 1-inaccessible universes ⋮ Partial Horn logic and Cartesian categories ⋮ Non-well-founded trees in categories ⋮ Coalgebras in a category of classes ⋮ Relating first-order set theories, toposes and categories of classes ⋮ A SYNTACTIC CHARACTERIZATION OF MORITA EQUIVALENCE ⋮ Derived rules for predicative set theory: an application of sheaves ⋮ Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets ⋮ Constructive toposes with countable sums as models of constructive set theory ⋮ Unnamed Item ⋮ Proof-relevance of families of setoids and identity in type theory ⋮ Algebraic set theory and the effective topos ⋮ The associated sheaf functor theorem in algebraic set theory ⋮ Aspects of predicative algebraic set theory. I: Exact completion ⋮ Aspects of predicative algebraic set theory. II: Realizability ⋮ W-types in homotopy type theory ⋮ Inductive types and exact completion ⋮ Unnamed Item ⋮ A Brief Introduction to Algebraic Set Theory ⋮ The generalised type-theoretic interpretation of constructive set theory ⋮ Lawvere–Tierney sheaves in Algebraic Set Theory ⋮ A minimalist two-level foundation for constructive mathematics ⋮ Wellfounded trees in categories ⋮ Type Theory and Homotopy ⋮ Heyting-valued interpretations for constructive set theory ⋮ Regular universes and formal spaces ⋮ The axiom of multiple choice and models for constructive set theory

Cites Work

• Constructivism in mathematics. An introduction. Volume I
• Sheaves in geometry and logic: a first introduction to topos theory
• Wellfounded trees in categories
• Intuitionistic choice and classical logic
• Constructive set theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Type theories, toposes and constructive set theory: Predicative aspects of AST