Constructive toposes with countable sums as models of constructive set theory

DOI10.1016/j.apal.2012.01.013zbMath1275.03145OpenAlexW2042711307MaRDI QIDQ448336

Thomas Streicher, Alex K. Simpson

Publication date: 6 September 2012

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

Full work available at URL: https://doi.org/10.1016/j.apal.2012.01.013

zbMATH Keywords

sheavesconstructive set theorycategorical logicconstructive toposCZF

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Relating first-order set theories, toposes and categories of classes
• Aspects of predicative algebraic set theory. II: Realizability
• Aspects of predicative algebraic set theory. I: Exact completion
• Realizability. An introduction to its categorical side
• Sheaf models for set theory
• Set theoretic foundations for constructive analysis
• Wellfounded trees in categories
• Independence results around constructive ZF
• A characterization of the left exact categories whose exact completions are toposes
• Aspects of predicative algebraic set theory III: sheaves
• Impredicativity entails untypedness
• A Unified Approach to Algebraic Set Theory
• Constructive set theory
• Type theories, toposes and constructive set theory: Predicative aspects of AST

This page was built for publication: Constructive toposes with countable sums as models of constructive set theory