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

DOI10.1016/J.APAL.2012.01.011zbMATH Open1257.03095arXiv1201.6272OpenAlexW2120588128MaRDI QIDQ448334FDOQ448334

Authors: Erik Palmgren 

Publication date: 6 September 2012

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

Abstract: Bishop's informal set theory is briefly discussed and compared to Lawvere's Elementary Theory of the Category of Sets (ETCS). We then present a constructive and predicative version of ETCS, whose standard model is based on the constructive type theory of Martin-L"of. The theory, CETCS, provides a structuralist foundation for constructive mathematics in the style of Bishop.

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

Recommendations

• scientific article; zbMATH DE number 2247250
• Exact completion and constructive theories of sets
• scientific article; zbMATH DE number 2172973
• Local constructive set theory and inductive definitions
• Comparing material and structural set theories

zbMATH Keywords

categorical logicconstructive type theoryBishop's informal set theorycategories of setsLawvere's elementary theory of the category of setsstructuralist foundation for constructive mathematics

Mathematics Subject Classification ID

Categories of sets, characterizations (18B05) Categorical logic, topoi (03G30) Topoi (18B25)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Constructive set theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• Modular correspondence between dependent type theories and categories including pretopoi and topoi
• Title not available (Why is that?)
• Wellfounded trees in categories
• Categorical set theory: A characterization of the category of sets
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• Avoiding the axiom of choice in general category theory
• Cantor's \textit{Grundlagen} and the paradoxes of set theory
• Exploring Categorical Structuralism
• Title not available (Why is that?)
• Locally cartesian closed categories without chosen constructions
• Inductive types and exact completion
• Title not available (Why is that?)

Cited In (17)

• Towards ``mouldable code via nested code graph transformation
• Title not available (Why is that?)
• Sets completely separated by functions in Bishop set theory
• Direct spectra of Bishop spaces and their limits
• Local constructive set theory and inductive definitions
• Proof-relevance in Bishop-style constructive mathematics
• On the local Cartesian closure of exact completions
• Title not available (Why is that?)
• Exact completion and constructive theories of sets
• Algebras of complemented subsets
• Categories with families and first-order logic with dependent sorts
• Infinite sets that satisfy the principle of omniscience in any variety of constructive mathematics
• A categorical reading of the numerical existence property in constructive foundations
• Constructive set theory with operations
• Title not available (Why is that?)
• Univalent foundations as structuralist foundations
• Comparing material and structural set theories

This page was built for publication: Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets

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