Identity types and weak factorization systems in Cauchy complete categories
Abstract It has been known that categorical interpretations of dependent type theory with Σ- and Id-types induce weak factorization systems. When one has a weak factorization system $({\cal L},{\cal R})$ on a category $\mathbb{C}$ in hand, it is then natural to ask whether or not $({\cal L},{\cal R})$ harbors an interpretation of dependent type theory with Σ- and Id- (and possibly Π-) types. Using the framework of display map categories to phrase this question more precisely, one would ask whether or not there exists a class ${\cal D}$ of morphisms of $\mathbb{C}$ such that the retract closure of ${\cal D}$ is the class ${\cal R}$ and the pair $(\mathbb{C},{\cal D})$ forms a display map category modeling Σ- and Id- (and possibly Π-) types. In this paper, we show, with the hypothesis that $\cal{C}$ is Cauchy complete, that there exists such a class $\cal{D}$ if and only if $(\mathbb{C},\cal{R})$ itself forms a display map category modeling Σ- and Id- (and possibly Π-) types. Thus, we reduce the search space of our original question from a potentially proper class to a singleton.