A category-theoretic version of the identity type weak factorization system
(English)Manuscript (preprint) (Other academic)
Gambino and Garner proved that the syntactic category of a dependent type theory with identity types can be endowed with a weak factorization system structure, called identity type weak factorization system. In this paper we consider an enrichment of Joyal's notion of tribe which allow us to prove a purely category-theoretic version of the identity type weak factorization system, thus generalizing Gambino and Garner's result. We investigate then how it relates with other well-known weak factorization systems, namely those arising from Quillen model structures on the category of topological spaces and on the category of small groupoids.
Algebra and Logic
IdentifiersURN: urn:nbn:se:su:diva-109909OAI: oai:DiVA.org:su-109909DiVA: diva2:769630