Constructive toposes with countable sums as models of constructive set theory
From MaRDI portal
Publication:448336
DOI10.1016/j.apal.2012.01.013zbMath1275.03145MaRDI 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
03G30: Categorical logic, topoi
18B25: Topoi
03E70: Nonclassical and second-order set theories
03F50: Metamathematics of constructive systems
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