We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
Homotopy theoretic models of identity types.
- Authors
AWODEY, STEVE; WARREN, MICHAEL A.
- Abstract
Quillen [ 17 ] 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 [ 15 ] or the work of Joyal [ 11 , 12 ] and Lurie [ 13 ] 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 [ 14 ] due to Hofmann and Streicher [ 9 ]. 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. [ 3 ] and [ 5 ]), this promise of applications is of a practical, as well as theoretical, nature.
- Subjects
HOMOTOPY theory; TOPOLOGY; MODEL categories (Mathematics); MATHEMATICAL logic; MATHEMATICS; TYPE theory; COMPUTERS; GEOMETRY
- Publication
Mathematical Proceedings of the Cambridge Philosophical Society, 2009, Vol 146, Issue 1, p45
- ISSN
0305-0041
- Publication type
Article
- DOI
10.1017/S0305004108001783