Constructivist and Structuralist Foundations: Bishop's and Lawvere's Theories of Sets

2012/01/30 by Erik Palmgren, Palmgren, Erik · 2 citations
Computer Science · Mathematics · #03B15 #03G30 #18B05 #18B25 #Advanced Algebra and Logic #Category Theory (math.CT) #Computability, Logic, AI Algorithms #FOS: Mathematics #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #math.CT #math.LO #msc:03B15 #msc:03G30 #msc:18B05 #msc:18B25

paper · pdf · doi:10.48550/arxiv.1201.6272

28 pages

arxiv created 2012/01/30 · openalex publication_date 2012/01/30 · arxiv updated 2012/01/31 · openalex created_date 2025/10/24 · openalex updated_date 2026/07/28

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öf. The theory, CETCS, provides a structuralist foundation for constructive mathematics in the style of Bishop.

Cited by

• Orthocomplemented subspaces and partial projections on a Hilbert space
• Coinductive well-foundedness

Related

• On the Existence and Disjunction Properties in Structural Set Theory
• Logics and Admissible Rules of Constructive Set Theories
• A construction of set theory
• Families of Sets in Bishop Set Theory
• Another New Foundation: A Theory with Combined Concepts from Set Theory, Type Theory and Leśniewski's Mereology