Jacopo Emmenegger: On the local cartesian closure of exact completions

Carboni and Rosolini have given a characterisation of (local) cartesian closure of exact completions which unfortunately doesn’t hold in full generality, as originally claimed.

We will discuss a sufficient condition for the local cartesian closure of an exact completion, which holds in full generality. This condition was inspired by an axiom of constructive set theory, and originally applied to a constructive version of Lawvere’s ETCS.
We will see however that it naturally arises in the homotopy-theoretic context as well. In particular, it can be used to conclude that the exact completion of the homotopy category of topological spaces is locally cartesian closed.