2. Homotopy Type Theory
We begin with a brief summary of the connection between homotopy theory and higher-dimensional category theory. In classical homotopy theory, a space is a set of points equipped with a topology, and a path between points and is represented by a continuous map , where and . This function can be thought of as giving a point in at each “moment in time”. For many purposes, strict equality of paths (meaning, pointwise equal functions) is too fine a notion. For example, one can define operations of path concatenation (if is a path from to and is a path from to , then the concatenation is a path from to ) and inverses ( is a path from to ). However, there are natural equations between these operations that do not hold for strict equality: for example, the path (which walks from to , and then back along the same route, as time goes from to ) is not strictly equal to the identity path (which stays still at at all times).
The remedy is to consider a coarser notion of equality of paths called homotopy. A homotopy between a pair of continuous maps and is a continuous map satisfying and . In the specific case of paths and from to , a homotopy is a continuous map such that and for all . In this case we require also that and for all , so that for each the function is again a path from to ; a homotopy of this sort is said to be endpoint-preserving or rel endpoints. Such a homotopy is the image in of a square that fills in the space between and , which can be thought of as a “continuous deformation” between and , or a 2-dimensional path between paths.
For example, because walks out and back along the same route, you know that you can continuously shrink down to the identity path—it won’t, for example, get snagged around a hole in the space. Homotopy is an equivalence relation, and operations such as concatenation, inverses, etc., respect it. Moreover, the homotopy equivalence classes of loops at some point (where two loops and are equated when there is a based homotopy between them, which is a homotopy as above that additionally satisfies for all ) form a group called the fundamental group. This group is an algebraic invariant of a space, which can be used to investigate whether two spaces are homotopy equivalent (there are continuous maps back and forth whose composites are homotopic to the identity), because equivalent spaces have isomorphic fundamental groups.
Because homotopies are themselves a kind of 2-dimensional path, there is a natural notion of 3-dimensional homotopy between homotopies, and then homotopy between homotopies between homotopies, and so on. This infinite tower of points, path, homotopies, homotopies between homotopies, …, equipped with algebraic operations such as the fundamental group, is an instance of an algebraic structure called a (weak) -groupoid. An -groupoid consists of a collection of objects, and then a collection of morphisms between objects, and then morphisms between morphisms, and so on, equipped with some complex algebraic structure; a morphism at level is called a -morphism. Morphisms at each level have identity, composition, and inverse operations, which are weak in the sense that they satisfy the groupoid laws (associativity of composition, identity is a unit for composition, inverses cancel) only up to morphisms at the next level, and this weakness gives rise to further structure. For example, because associativity of composition of morphisms is itself a higher-dimensional morphism, one needs an additional operation relating various proofs of associativity: the various ways to reassociate into give rise to Mac Lane’s pentagon. Weakness also creates non-trivial interactions between levels.
Every topological space has a fundamental -groupoid whose -morphisms are the -dimensional paths in . The weakness of the -groupoid corresponds directly to the fact that paths form a group only up to homotopy, with the -paths serving as the homotopies between the -paths. Moreover, the view of a space as an -groupoid preserves enough aspects of the space to do homotopy theory: the fundamental -groupoid construction is adjoint to the geometric realization of an -groupoid as a space, and this adjunction preserves homotopy theory (this is called the homotopy hypothesis/theorem, because whether it is a hypothesis or theorem depends on how you define -groupoid). For example, you can easily define the fundamental group of an -groupoid, and if you calculate the fundamental group of the fundamental -groupoid of a space, it will agree with the classical definition of fundamental group of that space. Because of this correspondence, homotopy theory and higher-dimensional category theory are intimately related.
Now, in homotopy type theory each type can be seen to have the structure of an -groupoid. Recall that for any type , and any , we have a identity type , also written or just . Logically, we may think of elements of as evidence that and are equal, or as identifications of with . Furthermore, type theory (unlike, say, first-order logic) allows us to consider such elements of also as individuals which may be the subjects of further propositions. Therefore, we can iterate the identity type: we can form the type of identifications between identifications , and the type , and so on. The structure of this tower of identity types corresponds precisely to that of the continuous paths and (higher) homotopies between them in a space, or an -groupoid.
Thus, we will frequently refer to an element as a path from to ; we call its start point and its end point. Two paths with the same start and end point are said to be parallel, in which case an element can be thought of as a homotopy, or a morphism between morphisms; we will often refer to it as a 2-path or a 2-dimensional path Similarly, is the type of 3-dimensional paths between two parallel 2-dimensional paths, and so on. If the type is “set-like”, such as , these iterated identity types will be uninteresting (see §3.1 (http://planetmath.org/31setsandntypes)), but in the general case they can model non-trivial homotopy types.
An important difference between homotopy type theory and classical homotopy theory is that homotopy type theory provides a synthetic description of spaces, in the following sense. Synthetic geometry is geometry in the style of Euclid : one starts from some basic notions (points and lines), constructions (a line connecting any two points), and axioms (all right angles are equal), and deduces consequences logically. This is in contrast with analytic geometry, where notions such as points and lines are represented concretely using cartesian coordinates in —lines are sets of points—and the basic constructions and axioms are derived from this representation. While classical homotopy theory is analytic (spaces and paths are made of points), homotopy type theory is synthetic: points, paths, and paths between paths are basic, indivisible, primitive notions.
Moreover, one of the amazing things about homotopy type theory is that all of the basic constructions and axioms—all of the higher groupoid structure—-arises automatically from the induction principle for identity types. Recall from §1.12 (http://planetmath.org/112identitytypes) that this says that if
for every and every we have a type , and
for every we have an element ,
there exists an element for every two elements and , such that .
In other words, given dependent functions
there is a dependent function
for every . Usually, every time we apply this induction rule we will either not care about the specific function being defined, or we will immediately give it a different name.
Informally, the induction principle for identity types says that if we want to construct an object (or prove a statement) which depends on an inhabitant of an identity type, then it suffices to perform the construction (or the proof) in the special case when and are the same (judgmentally) and is the reflexivity element (judgmentally). When writing informally, we may express this with a phrase such as “by induction, it suffices to assume…”. This reduction to the “reflexivity case” is analogous to the reduction to the “base case” and “inductive step” in an ordinary proof by induction on the natural numbers, and also to the “left case” and “right case” in a proof by case analysis on a disjoint union or disjunction.
The “conversion rule” (2.0.1) is less familiar in the context of proof by induction on natural numbers, but there is an analogous notion in the related concept of definition by recursion. If a sequence is defined by giving and specifying in terms of , then in fact the term of the resulting sequence is the given one, and the given recurrence relation relating to holds for the resulting sequence. (This may seem so obvious as to not be worth saying, but if we view a definition by recursion as an algorithm for calculating values of a sequence, then it is precisely the process of executing that algorithm.) The rule (2.0.1) is analogous: it says that if we define an object for all by specifying what the value should be when is , then the value we specified is in fact the value of .
This induction principle endows each type with the structure of an -groupoid, and each function between two types the structure of an -functor between two such groupoids. This is interesting from a mathematical point view, because it gives a new way to work with -groupoids. It is interesting from a type-theoretic point view, because it reveals new operations that are associated with each type and function. In the remainder of this chapter, we begin to explore this structure.
- 1 Euclid, Elements,Vols. 1–13 Elsevier,300 BC
|Title||2. Homotopy Type Theory|