Exact completion and constructive theories of sets

TL;DR

This paper explores the use of exact completions to analyze categorical properties of setoids and models of constructive set theories, focusing on categories with weak limits and their internal logic.

Contribution

It introduces a new approach to study categories lacking equalisers via exact completions, linking internal logic with models of CETCS.

Findings

Provides a sufficient condition for local cartesian closure of an exact completion.

Shows when an exact completion yields a model of CETCS.

Analyzes categories with weak limits in the context of constructive set theories.

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.