Natural Models of Homotopy Type Theory

paper

Natural models of homotopy type theory — Steve Awodey (2014; Math. Struct. Comp. Sci. (2016)). arXiv:1406.3219 (v4, PDF).

Reformulates categories with families as representable natural transformations of presheaves, and expresses the type formers of dependent type theory as operations on such a map, using the associated polynomial functor. Gives natural models of extensional and of homotopy type theory.

Sources: the paper, arXiv:1406.3219v4, checked against the arXiv listing. Index: Papers.

Key definitions and results

• Definition 1: representable natural transformation of presheaves
• Proposition 2: a representable map $p:\dot{\mathcal{U}}\to \mathcal{U}$ is the same as a cwf
• Theorem 16: natural models of extensional Martin-Löf type theory with $\Pi$, $\Sigma$ and identity types

Concept notes

Category with Families

Used in Sophia

Core Calculus