Aspects of predicative algebraic set theory. I: Exact completion

DOI10.1016/J.APAL.2008.06.013zbMath1165.03045arXiv0710.3077OpenAlexW2152342937MaRDI QIDQ958492

Ieke Moerdijk, Benno van den Berg

Publication date: 5 December 2008

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

Full work available at URL: https://arxiv.org/abs/0710.3077

zbMATH Keywords

constructive set theorycategorical logicexact completion

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Nonclassical and second-order set theories (03E70) Categories admitting limits (complete categories), functors preserving limits, completions (18A35) Metamathematics of constructive systems (03F50)

Related Items (11)

Relating first-order set theories, toposes and categories of classes ⋮ 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 ⋮ Comparing material and structural set theories ⋮ EXACT COMPLETION AND CONSTRUCTIVE THEORIES OF SETS ⋮ Aspects of predicative algebraic set theory. I: Exact completion ⋮ Aspects of predicative algebraic set theory. II: Realizability ⋮ Lawvere–Tierney sheaves in Algebraic Set Theory ⋮ Models of intuitionistic set theory in subtoposes of nested realizability toposes ⋮ The axiom of multiple choice and models for constructive set theory

Cites Work

• Unnamed Item
• Unnamed Item
• 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
• Inductive types and exact completion
• Coalgebras in a category of classes
• Cocomplete toposes whose exact completions are toposes
• The associated sheaf functor theorem in algebraic set theory
• Aspects of predicative algebraic set theory. I: Exact completion
• Lindenbaum algebras of intuitionistic theories and free categories
• Sheaf models for set theory
• The World's simplest axiom of choice fails
• Sheaves in geometry and logic: a first introduction to topos theory
• First order categorical logic. Model-theoretical methods in the theory of topoi and related categories
• Applications of sheaves. Proceedings of the research symposium on applications of sheaf theory to logic, algebra and analysis, Durham, July 9--21, 1977
• A completeness theorem for open maps
• Wellfounded trees in categories
• Artin glueing
• Some free constructions in realizability and proof theory
• CZF and second order arithmetic
• A fixpoint theorem for complete categories
• Heyting-valued interpretations for constructive set theory
• Relating First-Order Set Theories and Elementary Toposes
• Freyd’s models for the independence of the axiom of choice
• Models of non-well-founded sets via an indexed final coalgebra theorem
• Algebraic set theory and the effective topos
• The axiom of choice
• When do completion processes give rise to extensive categories?
• Type theories, toposes and constructive set theory: Predicative aspects of AST

This page was built for publication: Aspects of predicative algebraic set theory. I: Exact completion