Models of Martin-Löf type theory from algebraic weak factorisation systems

Abstract

We introduce type-theoretic algebraic weak factorisation systems and show how they give rise to homotopy-theoretic models of Martin-Löf type theory. This is done by showing that the comprehension category associated to a type-theoretic algebraic weak factorisation system satisfies the assumptions necessary to apply a right adjoint method for splitting comprehension categories. We then provide methods for constructing several examples of type-theoretic algebraic weak factorisation systems, encompassing the existing groupoid model and cubical sets models, as well as some models based on normal fibrations

Final version, accepted for publication in Journal of Symbolic Logic, 45 pages

References in corpus (5)

• Homotopy theoretic models of identity types
• The identity type weak factorisation system
• On the construction of functorial factorizations for model categories
• Towards a constructive simplicial model of Univalent Foundations
• Type-theoretic weak factorization systems

Cited by in corpus (1)

• Kripke-Joyal forcing for type theory and uniform fibrations