Categorical Homotopy Theory

Abstract

Categorical homotopy theory provides the precise mathematical framework for modeling homotopy type theory. We use structures from abstract homotopy theory, specifically model categories and $\infty$-toposes¹, to provide semantics for type-theoretic constructs such as Martin-Löf identity types and the univalence axiom.

Awodey-Warren Semantics

In the categorical interpretation, contexts and types are interpreted as objects and morphisms in a category equipped with a weak factorization system. Dependent types are modeled as fibrations.

Identity Type

An identity type $I{d}_A(x,y)$ is modeled using path objects in a model category. The reflexivity term corresponds to the weak equivalence in the factorization of the diagonal map $\Delta :A\to A\times A$, while the identity elimination rule (J-rule) is validated by the lifting property of fibrations against trivial cofibrations.

Simplicial and Cubical Models

We require specific combinatorial model categories to validate advanced features of homotopy type theory.

• Simplicial sets: The model structure on Kan complexes provides the standard univalent model of homotopy type theory. It validates the univalence axiom and higher inductive types but lacks computational content for univalence.
• Cubical sets: To restore constructive content and strict canonicity, we use model structures on presheaf categories over a cubical test category. This forms the basis of cubical type theory and its implementation in Agda.

Relation to Higher Toposes

Homotopy type theory serves as the internal language of $(\infty ,1)$-toposes¹. Just as extensional dependent type theory is the internal language of locally cartesian closed categories, extending the theory with the univalence axiom categorifies the semantics to the $\infty$-categorical² setting.

References

• Kapulkin, K., Lumsdaine, P. L., & Pelayo, A. The simplicial model of univalent foundations.
• Cohen, C., Coquand, T., Huber, S., & Mörtberg, A. Cubical type theory: a constructive interpretation of the univalence axiom.
• Shulman, M. Homotopy type theory: the logic of space.
• riehl2014-categorical-homotopy-theory

Footnotes

1. Infinity-Topos ↩ ↩²

2. Infinity Category Theory ↩