arXiv Open Access 2019

Identity types and weak factorization systems in Cauchy complete categories

Paige Randall North
Lihat Sumber

Abstrak

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.

Topik & Kata Kunci

Penulis (1)

P

Paige Randall North

Format Sitasi

North, P.R. (2019). Identity types and weak factorization systems in Cauchy complete categories. https://arxiv.org/abs/1901.03567

Akses Cepat

Lihat di Sumber
Informasi Jurnal
Tahun Terbit
2019
Bahasa
en
Sumber Database
arXiv
Akses
Open Access ✓