Exact completion and constructive theories of sets

Jacopo Emmenegger, Erik Palmgren

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 Constru…