Exact completion and constructive theories of sets

DOI10.1017/JSL.2020.2MaRDI QIDQ5148098zbMATH OpenOpenAlexFDO

Authors Jacopo Emmenegger, Erik Palmgren

Publication date 29 January 2021

Published in Journal of Symbolic Logic (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

categorical logicconstructive set theoryexact completionlocal Cartesian closuresetoids

Mathematics Subject Classification ID

Type theory (03B38) Intuitionistic mathematics (03F55) Categorical logic, topoi (03G30) Foundations, relations to logic and deductive systems (18A15) Categories admitting limits (complete categories), functors preserving limits, completions (18A35) Categories of sets, characterizations (18B05) Topoi (18B25) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15)

Abstract: In the present paper we use the theory of exact completions to study categorical properties of small setoids in Martin-L"of type theory and, more generally, of models of the Constructive Elementary Theory of the Category of Sets, in terms of properties of their subcategories of choice objects (i.e. objects satisfying the axiom of choice). Because of these intended applications, we deal with categories that lack equalisers and just have weak ones, but whose objects can be regarded as collections of global elements. In this context, we study the internal logic of the categories involved, and employ this analysis to give a sufficient condition for the local cartesian closure of an exact completion. Finally, we apply this result to show when an exact completion produces a model of CETCS.

Recommendations

• The fullness axiom and exact completion of homotopy categories
• Exact completion of path categories and algebraic set theory. I: Exact completion of path categories
• The derivator of setoids
• Category theoretic structure of setoids
• Constructing categories and setoids of setoids in type theory

Cites work

• A categorical version of the BrouwerHeytingKolmogorov interpretation
• Adjointness in Foundations
• Aspects of predicative algebraic set theory. I: Exact completion
• Colimit completions and the effective topos
• Constructing categories and setoids of setoids in type theory
• Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets
• Elementary quotient completion
• Exact completion of path categories and algebraic set theory. I: Exact completion of path categories
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 3754682 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 1251511 (Why is no real title available?)
• scientific article; zbMATH DE number 1123623 (Why is no real title available?)
• scientific article; zbMATH DE number 2079044 (Why is no real title available?)
• scientific article; zbMATH DE number 3794304 (Why is no real title available?)
• scientific article; zbMATH DE number 937370 (Why is no real title available?)
• scientific article; zbMATH DE number 1392302 (Why is no real title available?)
• scientific article; zbMATH DE number 3291139 (Why is no real title available?)
• Inductive types and exact completion
• Locally cartesian closed exact completions
• On the axiom of extensionality – Part I
• On the local Cartesian closure of exact completions
• Quotient completion for the foundation of constructive mathematics
• Regular and exact completions
• Relating quotient completions via categorical logic
• Setoids and universes
• Some free constructions in realizability and proof theory
• Weak subobjects and the epi-monic completion of a category.
• Wellfounded trees in categories

Cited in

(30)

• Cartesian closed exact completions
• Extensive forms and set-theoretic forms
• Complete topoi representing models of set theory
• Constructive sets in computable sets
• Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator
• Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe
• The completeness of arithmetic sets under operations of set theory
• Category theoretic structure of setoids
• Nonessential extensions of complete theories
• Equalisers of frames in constructive set theory
• Constructing categories and setoids of setoids in type theory
• Constructing a small category of setoids
• scientific article; zbMATH DE number 4204629 (Why is no real title available?)
• Quotient completion for the foundation of constructive mathematics
• scientific article; zbMATH DE number 4105274 (Why is no real title available?)
• Completeness of global intuitionistic set theory
• On existence of complete sets for bounded reducibilities
• Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets
• The fullness axiom and exact completion of homotopy categories
• W-types in setoids
• Constructive reflectivity principles for regular theories
• Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions
• Inductive types and exact completion
• scientific article; zbMATH DE number 2247250 (Why is no real title available?)
• The effective model structure and \(\infty\)-groupoid objects
• The derivator of setoids
• Flatness, weakly lex colimits, and free exact completions
• Constructions of complete sets
• The notion of exhaustiveness and Ascoli-type theorems
• Aspects of predicative algebraic set theory. I: Exact completion

Describes a project that uses

Uses Software

• GitHub

This page was built for publication: Exact completion and constructive theories of sets

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