# Models of Martin-L\"of type theory from algebraic weak factorisation systems

## TL;DR

This paper introduces a new algebraic framework for modeling Martin-Löf type theory using weak factorisation systems, enabling the construction of various homotopy-theoretic models including groupoid and cubical set models.

## Contribution

It develops the concept of type-theoretic algebraic weak factorisation systems and demonstrates their application in creating models of type theory, extending existing models and providing new construction methods.

## Key findings

- Established a correspondence between algebraic weak factorisation systems and models of type theory.
- Constructed examples including the groupoid and cubical set models.
- Provided methods for generating models based on normal fibrations.

## 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