pith. sign in

arxiv: 1901.03567 · v1 · pith:FO5FRHHDnew · submitted 2019-01-11 · 🧮 math.CT · cs.LO

Identity types and weak factorization systems in Cauchy complete categories

classification 🧮 math.CT cs.LO
keywords classsigma-typescategorydisplayfactorizationpossiblyweak
0
0 comments X
read the original 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.

This paper has not been read by Pith yet.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.