Homotopy type theory


Homotopy type theory (HoTT) interprets type theoryPlanetmathPlanetmath from a homotopical perspective. In homotopy type theory, we regard the types as “spaces” (as studied in homotopy theory) or higher groupoidsPlanetmathPlanetmathPlanetmath, and the logical constructions (such as the productPlanetmathPlanetmathPlanetmathPlanetmath A×B) as homotopy-invariant constructions on these spaces. In this way, we are able to manipulate spaces directly without first having to develop point-set topology (or any combinatorial replacement for it, such as the theory of simplicial sets). To briefly explain this perspective, consider first the basic concept of type theory, namely that the term a is of type A, which is written:

a:A.

This expression is traditionally thought of as akin to:

a is an element of the set A.”

However, in homotopy type theory we think of it instead as:

a is a point of the space A.”

Similarly, every function f:AB in type theory is regarded as a continuous map from the space A to the space B.

We should stress that these “spaces” are treated purely homotopically, not topologically. For instance, there is no notion of “open subset” of a type or of “convergence” of a sequenceMathworldPlanetmathPlanetmath of elements of a type. We only have “homotopical” notions, such as paths between points and homotopiesMathworldPlanetmath between paths, which also make sense in other models of homotopy theory (such as simplicial sets). Thus, it would be more accurate to say that we treat types as -groupoids; this is a name for the “invariant objects” of homotopy theory which can be presented by topological spacesMathworldPlanetmath, simplicial sets, or any other model for homotopy theory. However, it is convenient to sometimes use topological words such as “space” and “path”, as long as we remember that other topological concepts are not applicable.

(It is tempting to also use the phrase homotopy typeMathworldPlanetmath for these objects, suggesting the dual interpretationMathworldPlanetmathPlanetmath of “a type (as in type theory) viewed homotopically” and “a space considered from the point of view of homotopy theory.” The latter is a bit different from the classical meaning of “homotopy type” as an equivalence classMathworldPlanetmathPlanetmath of spaces modulo homotopy equivalenceMathworldPlanetmath, although it does preserve the meaning of phrases such as “these two spaces have the same homotopy type”.)

The idea of interpreting types as structured objects, rather than sets, has a long pedigree, and is known to clarify various mysterious aspects of type theory. For instance, interpreting types as sheaves helps explain the intuitionistic nature of type-theoretic logic, while interpreting them as partial equivalence relations or “domains” helps explain its computational aspects. It also implies that we can use type-theoretic reasoning to study the structured objects, leading to the rich field of categorical logic. The homotopical interpretation fits this same pattern: it clarifies the nature of identityPlanetmathPlanetmathPlanetmath (or equality) in type theory, and allows us to use type-theoretic reasoning in the study of homotopy theory.

The key new idea of the homotopy interpretation is that the logical notion of identity a=b of two objects a,b:A of the same type A can be understood as the existence of a path p:ab from point a to point b in the space A. This also means that two functions f,g:AB can be identified if they are homotopicMathworldPlanetmath, since a homotopy is just a (continuous) family of paths px:f(x)g(x) in B, one for each x:A. In type theory, for every type A there is a (formerly somewhat mysterious) type 𝖨𝖽A of identifications of two objects of A; in homotopy type theory, this is just the path space AI of all continuous maps IA from the unit interval. In this way, a term p:𝖨𝖽A(a,b) represents a path p:ab in A.

The idea of homotopy type theory arose around 2006 in independent work by Awodey and Warren [1] and Voevodsky [3], but it was inspired by Hofmann and Streicher’s earlier groupoid interpretation [2]. Indeed, higher-dimensional category theoryMathworldPlanetmathPlanetmathPlanetmathPlanetmath (particularly the theory of weak -groupoids) is now known to be intimately connectedPlanetmathPlanetmath to homotopy theory, as proposed by Grothendieck and now being studied intensely by mathematicians of both sorts. The original semantic models of Awodey–Warren and Voevodsky use well-known notions and techniques from homotopy theory which are now also in use in higher category theory, such as Quillen model categories and Kan simplicial sets.

Voevodsky recognized that the simplicial interpretation of type theory satisfies a further crucial property, dubbed univalence, which had not previously been considered in type theory (although Church’s principle of extensionality for propositionsPlanetmathPlanetmath turns out to be a very special case of it). Adding univalence to type theory in the form of a new axiom has far-reaching consequences, many of which are natural, simplifying and compelling. The univalence axiom also further strengthens the homotopical view of type theory, since it holds in the simplicial model and other related models, while failing under the view of types as sets.

References

  • 1 Steve Awodey and Michael A. Warren. Homotopy theoretic models of identity types. Mathematical Proceedings of the Cambridge Philosophical Society, 146:45–55 2009
  • 2 Hofmann,Martin and Streicher,Thomas. The groupoid interpretation of type theory. In Twenty-five years of constructive type theory (Venice,1995),volume 36 of Oxford Logic Guides, pages 83–111. Oxford University Press, 1998.
  • 3 Vladimir Voevodsky,Date-Modified. A very short note on the homotopy λ-calculus. \urlhttp://www.math.ias.edu/ vladimir/Site3/Univalent_Foundations_files/Hlambda_short_current.pdf, 2006.
Title Homotopy type theory
\metatable