Natural models of homotopy type theory

TL;DR

This paper characterizes natural models of homotopy type theory using category theory, showing their equivalence to categories with families and identifying conditions for modeling key type-theoretic constructs.

Contribution

It establishes a precise categorical framework for natural models of homotopy type theory and links them to axiomatic homotopy-theoretic structures.

Findings

Natural models correspond to categories with families.

Conditions for modeling dependent sums, products, and identity types are identified.

Many homotopy-theoretic settings admit such models.

Abstract

The notion of a natural model of type theory is defined in terms of that of a representable natural transfomation of presheaves. It is shown that such models agree exactly with the concept of a category with families in the sense of Dybjer, which can be regarded as an algebraic formulation of type theory. We determine conditions for such models to satisfy the inference rules for dependent sums, dependent products, and intensional identity types, as used in homotopy type theory. It is then shown that a category admits such a model if it has a class of maps that behave like the abstract fibrations in axiomatic homotopy theory: they should be stable under pullback, closed under composition and relative products, and there should be weakly orthogonal factorizations into the class. It follows that many familiar settings for homotopy theory also admit natural models of the basic system of homotopy type theory.