Giuseppe Rosolini

November 17, 2015
  1. 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.