Models of Martin-L\"of type theory from algebraic weak factorisation systems
Category Theory
2022-06-30 v3 Logic
Abstract
We introduce type-theoretic algebraic weak factorisation systems and show how they give rise to homotopy-theoretic models of Martin-L\"of 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
Keywords
Cite
@article{arxiv.1906.01491,
title = {Models of Martin-L\"of type theory from algebraic weak factorisation systems},
author = {Nicola Gambino and Marco Federico Larrea},
journal= {arXiv preprint arXiv:1906.01491},
year = {2022}
}
Comments
Final version, accepted for publication in Journal of Symbolic Logic, 45 pages