Exact completion and constructive theories of sets

Journal of Symbolic Logic 85 (2):563-584 (2020)
  Copy   BIBTEX

Abstract

In the present paper we use the theory of exact completions to study categorical properties of small setoids in Martin-Löf 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. 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.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,616

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

How to Understand the Completion of Art.Patrick Grafton-Cardwell - 2020 - Journal of Aesthetics and Art Criticism 78 (2):197-208.
The constructive completion of the space?Satoru Yoshida - 2005 - Mathematical Logic Quarterly 51 (1):77-82.
Exact calculation of inverse functions.Josef Berger - 2005 - Mathematical Logic Quarterly 51 (2):201-205.
Quotient topologies in constructive set theory and type theory.Hajime Ishihara & Erik Palmgren - 2006 - Annals of Pure and Applied Logic 141 (1):257-265.
Elementary Constructive Operational Set Theory.Andrea Cantini & Laura Crosilla - 2010 - In Ralf Schindler (ed.), Ways of Proof Theory. De Gruyter. pp. 199-240.
Inductive types and exact completion.Benno van den Berg - 2005 - Annals of Pure and Applied Logic 134 (2-3):95-121.
Set theory: Constructive and intuitionistic ZF.Laura Crosilla - 2010 - Stanford Encyclopedia of Philosophy.
Metric complements of overt closed sets.Thierry Coquand, Erik Palmgren & Bas Spitters - 2011 - Mathematical Logic Quarterly 57 (4):373-378.
Constructive complements of unions of two closed sets.Douglas S. Bridges - 2004 - Mathematical Logic Quarterly 50 (3):293.

Analytics

Added to PP
2020-06-18

Downloads
12 (#929,405)

6 months
1 (#1,040,386)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Jacopo Emmenegger
Università degli Studi di Genova

Citations of this work

No citations found.

Add more citations

References found in this work

Adjointness in Foundations.F. William Lawvere - 1969 - Dialectica 23 (3‐4):281-296.
Wellfounded trees in categories.Ieke Moerdijk & Erik Palmgren - 2000 - Annals of Pure and Applied Logic 104 (1-3):189-218.

View all 9 references / Add more references