# Identity types and weak factorization systems in Cauchy complete categories

## TL;DR

This paper characterizes when a weak factorization system in a Cauchy complete category can interpret dependent type theory with Sigma- and Id-types, reducing the problem to a specific display map category.

## Contribution

It provides a necessary and sufficient condition for a weak factorization system to support dependent type theory interpretations in Cauchy complete categories.

## Key findings

- Characterizes when (C, R) forms a display map category for Sigma- and Id-types
- Reduces the search for suitable classes D to a unique candidate
- Establishes a criterion linking weak factorization systems and type-theoretic models

## Abstract

It has been known that categorical interpretations of dependent type theory with Sigma- 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 Sigma- and Id- (and possibly Pi-) 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 Sigma- and Id- (and possibly Pi-) 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 Sigma- and Id- (and possibly Pi-) types. Thus, we reduce the search space of our original question from a potentially proper class to a singleton.