Awodey, Warren: Homotopy theoretic models of identity types

Steve Awodey, Michael Warren: Homotopy theoretic models of identity types. Mathematical Proceedings of the Cambridge Philosophical Society, 2009. Available as arXiv:0709.0248.

Abstract: 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 and Lurie on quasicategories seems 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, this promise of applications is of a practical, as well as theoretical, nature. The present paper provides a precise indication of this connection between homotopy theory and logic; a more detailed discussion of these and further results will be given in Michael Warren’s Ph.D. dissertation.

@article {MR2461866,
    author = {Awodey, Steve and Warren, Michael A.},
     TITLE = {Homotopy theoretic models of identity types},
   JOURNAL = {Math. Proc. Cambridge Philos. Soc.},
  FJOURNAL = {Mathematical Proceedings of the Cambridge
              Philosophical Society},
    VOLUME = {146},
      YEAR = {2009},
    NUMBER = {1},
     PAGES = {45--55},
      ISSN = {0305-0041},
     CODEN = {MPCPCO},
   MRCLASS = {03B15 (03B35 18Gxx 55Uxx 68T15)},
  MRNUMBER = {2461866},
       DOI = {10.1017/S0305004108001783},
       URL = {http://dx.doi.org/10.1017/S0305004108001783},
    eprint = {0709.0248},
}

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s