Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets

DOI10.1016/j.apal.2012.01.011zbMath1257.03095arXiv1201.6272MaRDI QIDQ448334

Erik Palmgren

Publication date: 6 September 2012

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

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

zbMATH Keywords

constructive type theory; categorical logic; Bishop's informal set theory; categories of sets; Lawvere's elementary theory of the category of sets; structuralist foundation for constructive mathematics

Mathematics Subject Classification ID

03G30: Categorical logic, topoi

18B25: Topoi

18B05: Categories of sets, characterizations

Related Items

Proof-relevance in Bishop-style constructive mathematics, Direct spectra of Bishop spaces and their limits, EXACT COMPLETION AND CONSTRUCTIVE THEORIES OF SETS, Towards ``mouldable code via nested code graph transformation, Univalent foundations as structuralist foundations, Comparing material and structural set theories, Algebras of complemented subsets, On the local Cartesian closure of exact completions, Categories with families and first-order logic with dependent sorts, Infinite sets that Satisfy the Principle of Omniscience in any Variety of Constructive Mathematics

Cites Work

• Inductive types and exact completion
• Aspects of predicative algebraic set theory. I: Exact completion
• Wellfounded trees in categories
• Categorical set theory: A characterization of the category of sets
• Avoiding the axiom of choice in general category theory
• Modular correspondence between dependent type theories and categories including pretopoi and topoi
• Constructive set theory
• Exploring Categorical Structuralism
• Type theories, toposes and constructive set theory: Predicative aspects of AST
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item