Jacopo Emmenegger: A weak factorization system between type theory and homotopy theory

Gambino and Garner have proved that the rules of the identity type in Martin-Löf type theory imply the existence of a weak factorization system in the syntactic category, known as the identity type w.f.s. We present a generalization of this result to a category satisfying four axioms reminiscent of the rules of Martin-Löf type theory, and show that it applies also to the category of small groupoids and to that one of topological spaces, giving back the weak factorization systems generated by Grothendieck fibrations and by Hurewicz fibrations, respectively. The categorical setting also highlights a close connection between Paulin-Mohring rules for the identity type and the identity type w.f.s.

Some familiarity with dependent type theory and basic homotopy theory will be assumed.