Homotopy Theoretic Models of Identity Types
journal contributionposted on 03.10.2007, 00:00 by Steven Awodey, Michael A. Warren
Quillen  introduced model categories as an abstract framework for homotopy theory which would apply to a wide range of mathematical settings. By all accounts this program has been a success and—as, e.g., the work of Voevodsky on the homotopy theory of schemes  or the work of Joyal [11, 12] and Lurie  on quasicategories seem to indicate—it will likely continue to facilitate mathematical advances. In this paper we present a novel connection between model categories and mathematical logic, inspired by the groupoid model of (intensional) Martin–Löf type theory  due to Hofmann and Streicher . In particular, we show that a form of Martin–Löf type theory can be soundly modelled in any model category. This result indicates moreover that any model category has an associated “internal language” which is itself a form of Martin-Löf type theory. This suggests applications both to type theory and to homotopy theory. Because Martin–Löf type theory is, in one form or another, the theoretical basis for many of the computer proof assistants currently in use, such as Coq and Agda (cf.  and ), this promise of applications is of a practical, as well as theoretical, nature.