- November 2015
Exact completions, homotopical quotients, and type theory
We retrace an idea of Aurelio Carboni that the equivalence determining the maps of an exact completion is obtained from a homotopy. We show that the exact completion of a locos A is the homotopical quotient of a category of 2-groupoids on A with respect to a specific notion of interval. We connect this to the construction of models of type theory.