Models of Martin-Löf type theory from algebraic weak factorisation systems
arXiv:1906.01491 · doi:10.1017/jsl.2021.39
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
arXiv commentFinal version, accepted for publication in Journal of Symbolic Logic, 45 pages
References in corpus (13)
- Understanding the small object argument
- Homotopy theoretic models of identity types
- The identity type weak factorisation system
- Algebraic weak factorisation systems I: accessible AWFS
- The local universes model: an overlooked coherence construction for dependent type theories
- Algebraic model structures
- The Frobenius Condition, Right Properness, and Uniform Fibrations
- Algebraic weak factorisation systems II: categories of weak maps
- On the construction of functorial factorizations for model categories
- The theory and practice of Reedy categories
- Towards a constructive simplicial model of Univalent Foundations
- The Equivalence Extension Property and Model Structures
- Type-theoretic weak factorization systems