Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets
From MaRDI portal
(Redirected from Publication:448334)
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.
Recommendations
Cites work
- scientific article; zbMATH DE number 3754682 (Why is no real title available?)
- scientific article; zbMATH DE number 3521950 (Why is no real title available?)
- scientific article; zbMATH DE number 1216133 (Why is no real title available?)
- scientific article; zbMATH DE number 2079044 (Why is no real title available?)
- scientific article; zbMATH DE number 2172009 (Why is no real title available?)
- scientific article; zbMATH DE number 2172973 (Why is no real title available?)
- scientific article; zbMATH DE number 1913781 (Why is no real title available?)
- scientific article; zbMATH DE number 2117177 (Why is no real title available?)
- scientific article; zbMATH DE number 813127 (Why is no real title available?)
- scientific article; zbMATH DE number 3291139 (Why is no real title available?)
- scientific article; zbMATH DE number 3325567 (Why is no real title available?)
- scientific article; zbMATH DE number 2247253 (Why is no real title available?)
- 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
- Categorical set theory: A characterization of the category of sets
- Constructive set theory
- Exploring Categorical Structuralism
- Inductive types and exact completion
- Locally cartesian closed categories without chosen constructions
- Modular correspondence between dependent type theories and categories including pretopoi and topoi
- Type theories, toposes and constructive set theory: Predicative aspects of AST
- Wellfounded trees in categories
Cited in
(17)- Towards ``mouldable code via nested code graph transformation
- scientific article; zbMATH DE number 4177052 (Why is no real title available?)
- 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
- scientific article; zbMATH DE number 1693440 (Why is no real title available?)
- Exact completion and constructive theories of sets
- Algebras of complemented subsets
- Categories with families and first-order logic with dependent sorts
- A categorical reading of the numerical existence property in constructive foundations
- Infinite sets that satisfy the principle of omniscience in any variety of constructive mathematics
- Constructive set theory with operations
- Univalent foundations as structuralist foundations
- scientific article; zbMATH DE number 2247250 (Why is no real title available?)
- 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)
