In:
The Journal of Symbolic Logic, Cambridge University Press (CUP), Vol. 85, No. 2 ( 2020-06), p. 563-584
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 ( 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.
Type of Medium:
Online Resource
ISSN:
0022-4812
,
1943-5886
Language:
English
Publisher:
Cambridge University Press (CUP)
Publication Date:
2020
detail.hit.zdb_id:
2010607-5
SSG:
5,1
SSG:
17,1
Permalink