Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets
type: Item
instance of: scholarly article
title: Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets
zbMATH Open document ID: 1257.03095
author: Erik Palmgren
published in: Annals of Pure and Applied Logic
publication date: 2012-09-06T00:00:00Z
full work available at URL: https://arxiv.org/abs/1201.6272
reviewed by: Marco Benini
Mathematics Subject Classification ID: 03G30
Mathematics Subject Classification ID: 03B15
Mathematics Subject Classification ID: 18B05
Mathematics Subject Classification ID: 18B25
zbMATH DE Number: 6078321
zbMATH Keywords: categories of sets
zbMATH Keywords: categorical logic
zbMATH Keywords: Bishop's informal set theory
zbMATH Keywords: Lawvere's elementary theory of the category of sets
zbMATH Keywords: constructive type theory
zbMATH Keywords: structuralist foundation for constructive mathematics
MaRDI profile type: Publication
OpenAlex ID: W2120588128
arXiv ID: 1201.6272
cites work: Q3937387
cites work: Q4680361
cites work: Q5573965
cites work: Q5604461
cites work: Q4474857
cites work: Q4828514
cites work: Q4853985
cites work: Q4679166
cites work: Q4807625
cites work: Q4215784
cites work: Modular correspondence between dependent type theories and categories including pretopoi and topoi
cites work: Q5718565
cites work: Q4099613
cites work: Exploring Categorical Structuralism
cites work: Avoiding the axiom of choice in general category theory
cites work: Wellfounded trees in categories
cites work: Type theories, toposes and constructive set theory: Predicative aspects of AST
cites work: Constructive set theory
cites work: Categorical set theory: A characterization of the category of sets
cites work: Q5454624
cites work: Cantor's \textit{Grundlagen} and the paradoxes of set theory
cites work: Inductive types and exact completion
cites work: Aspects of predicative algebraic set theory. I: Exact completion
DOI: 10.1016/J.APAL.2012.01.011
review text: Comparing Bishop's informal set theory with Lawvere's elementary theory of the category of sets (ETCS), the author proposes 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.NEWLINENEWLINEAs one may expect, CETCS is classically equivalent to ETCS plus the Axiom of Choice and the Principle of Excluded Middle. Also, the theory allows to ``reason using elements'' which greatly simplifies its potential application, avoiding most of the rather complex categorical notions.NEWLINENEWLINENevertheless, a purely categorical characterisation of categorical models for CETCS is possible and the author shows it. This characterisation requires to show that the category is locally Cartesian closed, among a few other properties. Since deciding whether a category is locally Cartesian closed apparently requires the use of the Axiom of Choice in the meta-theory, the author reduces this check to the simpler task of verifying the validity of a specific axiom of CETCS. This last result has an independent value from CETCS and may be useful in other contexts.
description: scientific article; zbMATH DE number 6078321