Homotopy type theory

In mathematical logic and computer science, homotopy type theory (HoTT /hɒt/) refers to various lines of development of intuitionistic type theory, based on the interpretation of types as objects to which the intuition of (abstract) homotopy theory applies. In mathematical logic and computer science, homotopy type theory (HoTT /hɒt/) refers to various lines of development of intuitionistic type theory, based on the interpretation of types as objects to which the intuition of (abstract) homotopy theory applies. This includes, among other lines of work, the construction of homotopical and higher-categorical models for such type theories; the use of type theory as a logic (or internal language) for abstract homotopy theory and higher category theory; the development of mathematics within a type-theoretic foundation (including both previously existing mathematics and new mathematics that homotopical types make possible); and the formalization of each of these in computer proof assistants. There is a large overlap between the work referred to as homotopy type theory, and as the univalent foundations project. Although neither is precisely delineated, and the terms are sometimes used interchangeably, the choice of usage also sometimes corresponds to differences in viewpoint and emphasis. As such, this article may not represent the views of all researchers in the fields equally. This kind of variability is unavoidable when a field is in rapid flux. At one time the idea that types in intensional type theory with their identity types could be regarded as groupoids was mathematical folklore. It was first made precise semantically in the 1998 paper of Martin Hofmann and Thomas Streicher called 'The groupoid interpretation of type theory', in which they showed that intensional type theory had a model in the category of groupoids. This was the first truly 'homotopical' model of type theory, albeit only '1-dimensional' (the traditional models in the category of sets being homotopically 0-dimensional). Their paper also foreshadowed several later developments in homotopy type theory. For instance, they noted that the groupoid model satisfies a rule they called 'universe extensionality', which is none other than the restriction to 1-types of the univalence axiom that Vladimir Voevodsky proposed ten years later. (The axiom for 1-types is notably simpler to formulate, however, since a coherence notion of 'equivalence' is not required.) They also defined 'categories with isomorphism as equality' and conjectured that in a model using higher-dimensional groupoids, for such categories one would have 'equivalence is equality'; this was later proven by Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman. The first higher-dimensional models of intensional type theory were constructed by Steve Awodey and his student Michael Warren in 2005 using Quillen model categories. These results were first presented in public at the conference FMCS 2006 at which Warren gave a talk titled 'Homotopy models of intensional type theory', which also served as his thesis prospectus (the dissertation committee present were Awodey, Nicola Gambino and Alex Simpson). A summary is contained in Warren's thesis prospectus abstract. At a subsequent workshop about identity types at Uppsala University in 2006 there were two talks about the relation between intensional type theory and factorization systems: one by Richard Garner, 'Factorisation systems for type theory', and one by Michael Warren, 'Model categories and intensional identity types'. Related ideas were discussed in the talks by Steve Awodey, 'Type theory of higher-dimensional categories', and Thomas Streicher, 'Identity types vs. weak omega-groupoids: some ideas, some problems'. At the same conference Benno van den Berg gave a talk titled 'Types as weak omega-categories' where he outlined the ideas that later became the subject of a joint paper with Richard Garner. All early constructions of higher dimensional models had to deal with the problem of coherence typical of models of dependent type theory, and various solutions were developed. One such was given in 2009 by Voevodsky, another in 2010 by van den Berg and Garner. A general solution, building on Voevodsky's construction, was eventually given by Lumsdaine and Warren in 2014. At the PSSL86 in 2007 Awodey gave a talk titled 'Homotopy type theory' (this was the first public usage of that term, which was coined by Awodey). Awodey and Warren summarized their results in the paper 'Homotopy theoretic models of identity types', which was posted on the ArXiv preprint server in 2007 and published in 2009; a more detailed version appeared in Warren's thesis 'Homotopy theoretic aspects of constructive type theory' in 2008.