Constructive toposes with countable sums as models of constructive set theory

DOI10.1016/J.APAL.2012.01.013zbMATH Open1275.03145OpenAlexW2042711307MaRDI QIDQ448336FDOQ448336

Thomas Streicher, Alex 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

Recommendations

• scientific article; zbMATH DE number 2247250
• The axiom of multiple choice and models for constructive set theory
• scientific article; zbMATH DE number 2247251
• Kripke models for subtheories of \textsf{CZF}
• Generalizing realizability and Heyting models for constructive set theory

zbMATH Keywords

categorical logicsheavesconstructive set theoryconstructive toposCZF

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (5)

• Type theories, toposes and constructive set theory: Predicative aspects of AST
• Title not available (Why is that?)
• Title not available (Why is that?)
• Small decidable sheaves
• Title not available (Why is that?)

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q448336)