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 (L, R) on a category C in hand, it is then natural to ask whether or not (L, 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 D of morphisms of C such that the retract closure of D is the class R and the pair (C, D) forms a display map category modeling ∑- and Id- (and possibly ∏-) types. In this paper, we show, with the hypothesis that C is Cauchy complete, that there exists such a class D if and only if (C, 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.