8. Homotopy theory


In this chapter, we develop some homotopy theory within type theoryPlanetmathPlanetmath. We use the synthetic approach to homotopy theory introduced in \crefcha:basics: Spaces, points, paths, and homotopiesMathworldPlanetmathPlanetmath are basic notions, which are represented by types and elements of types, particularly the identity type. The algebraic structurePlanetmathPlanetmath of paths and homotopies is represented by the natural -groupoidPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath structureMathworldPlanetmath on types, which is generated by the rules for the identity type. Using higher inductive types, as introduced in \crefcha:hits, we can describe spaces directly by their universal propertiesMathworldPlanetmath.

There are several interesting aspects of this synthetic approach. First, it combines advantages of concrete models (such as topological spacesMathworldPlanetmath or simplicial sets) with advantages of abstract categorical frameworks for homotopy theory (such as Quillen model categories). On the one hand, our proofs feel elementary, and refer concretely to points, paths, and homotopies in types. On the other hand, our approach nevertheless abstracts away from any concrete presentationMathworldPlanetmathPlanetmathPlanetmath of these objects — for example, associativity of path concatenation is proved by path inductionMathworldPlanetmath, rather than by reparametrization of maps [0,1]X or by horn-filling conditions. Type theory seems to be a very convenient way to study the abstract homotopy theory of -groupoids: by using the rules for the identity type, we can avoid the complicated combinatorics involved in many definitions of -groupoids, and explicate only as much of the structure as is needed in any particular proof.

The abstract nature of type theory means that our proofs apply automatically in a varietyMathworldPlanetmathPlanetmath of settings. In particular, as mentioned previously, homotopy type theory has one interpretationMathworldPlanetmath in Kan simplicial sets, which is one model for the homotopy theory of -groupoids. Thus, our proofs apply to this model, and transferring them along the geometric realization functorMathworldPlanetmath from simplicial sets to topological spaces gives proofs of corresponding theorems in classical homotopy theory. However, though the details are work in progress, we can also interpret type theory in a wide variety of other categoriesMathworldPlanetmath that look like the category of -groupoids, such as (,1)-toposes. Thus, proving a result in type theory will show that it holds in these settings as well. This sort of extra generality is well-known as a property of ordinary categorical logic: univalent foundations extends it to homotopy theory as well.

Second, our synthetic approach has suggested new type-theoretic methods and proofs. Some of our proofs are fairly direct transcriptions of classical proofs. Others have a more type-theoretic feel, and consist mainly of calculations with -groupoid operationsMathworldPlanetmath, in a style that is very similarPlanetmathPlanetmath to how computer scientists use type theory to reason about computer programs. One thing that seems to have permitted these new proofs is the fact that type theory emphasizes different aspects of homotopy theory than other approaches: while tools like path induction and the universal properties of higher inductives are available in a setting like Kan simplicial sets, type theory elevates their importance, because they are the only primitive tools available for working with these types. Focusing on these tools had led to new descriptions of familiar constructions such as the universal coverMathworldPlanetmath of the circle and the Hopf fibration, using just the recursion principles for higher inductive types. These descriptions are very direct, and many of the proofs in this chapter involve computational calculations with such fibrationsMathworldPlanetmath. Another new aspect of our proofs is that they are constructive (assuming univalence and higher inductives types are constructive); we describe an application of this to homotopy groups of spheres in \crefsec:moreresults.

Third, our synthetic approach is very amenable to computer-checked proofs in proof assistants such as Coq and Agda. Almost all of the proofs described in this chapter have been computer-checked, and many of these proofs were first given in a proof assistant, and then “unformalized” for this book. The computer-checked proofs are comparable in length and effort to the informal proofs presented here, and in some cases they are even shorter and easier to do.

Before turning to the presentation of our results, we briefly review some basic concepts and theorems from homotopy theory for the benefit of the reader who is not familiar with them. We also give an overview of the results proved in this chapter.

Homotopy theory is a branch of algebraic topology, and uses tools from abstract algebra, such as group theory, to investigate properties of spaces. One question homotopy theorists investigate is how to tell whether two spaces are the same, where “the same” means homotopy equivalenceMathworldPlanetmathPlanetmath (continuous maps back and forth that compose to the identityPlanetmathPlanetmathPlanetmathPlanetmath up to homotopy—this gives the opportunity to “correct” maps that don’t exactly compose to the identity). One common way to tell whether two spaces are the same is to calculate algebraic invariants associated with a space, which include its homotopy groupsMathworldPlanetmath and homologyMathworldPlanetmathPlanetmath and cohomology groupsPlanetmathPlanetmath. EquivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath spaces have isomorphicPlanetmathPlanetmathPlanetmath homotopy/(co)homology groups, so if two spaces have different groups, then they are not equivalent. Thus, these algebraic invariants provide global information about a space, which can be used to tell spaces apart, and complements the local information provided by notions such as continuity. For example, the torus locally looks like the 2-sphere, but it has a global differencePlanetmathPlanetmath, because it as a hole in it, and this difference is visible in the homotopy groups of these two spaces.

The simplest example of a homotopy group is the fundamental groupMathworldPlanetmathPlanetmath of a space, which is written π1(X,x0): Given a space X and a point x0 in it, one can make a group whose elements are loops at x0 (continuous paths from x0 to x0), considered up to homotopy, with the group operations given by the identity path (standing still), path concatenation, and path reversal. For example, the fundamental group of the 2-sphere is trivial, but the fundamental group of the torus is not, which shows that the sphere and the torus are not homotopy equivalent. The intuition is that every loop on the sphere is homotopicMathworldPlanetmath to the identity, because its inside can be filled in. In contrast, a loop on the torus that goes through the donut’s hole is not homotopic to the identity, so there are non-trivial elements in the fundamental group.

The higher homotopy groups provide additional information about a space. Fix a point x0 in X, and consider the constant path 𝗋𝖾𝖿𝗅x0. Then the homotopy classes of homotopies between 𝗋𝖾𝖿𝗅x0 and itself form a group π2(X,x0), which tells us something about the two-dimensional structure of the space. Then π3(X,x0) is the group of homotopy classes of homotopies between homotopies, and so on. One of the basic problems of algebraic topology is calculating the homotopy groups of a space X, which means giving a group isomorphism between πk(X,x0) and some more direct description of a group (e.g., by a multiplication table or presentation). Somewhat surprisingly, this is a very difficult question, even for spaces as simple as the spheres. As can be seen from \creftab:homotopy-groups-of-spheres, some patterns emerge in the higher homotopy groups of spheres, but there is no general formulaMathworldPlanetmath, and many homotopy groups of spheres are currently still unknown.

\definecolor

xA\OPTcolormodel\OPTcolxA \definecolorxB\OPTcolormodel\OPTcolxB \definecolorxC\OPTcolormodel\OPTcolxC \definecolorxD\OPTcolormodel\OPTcolxD \definecolorxE\OPTcolormodel\OPTcolxE \definecolorxF\OPTcolormodel\OPTcolxF \definecolorxG\OPTcolormodel\OPTcolxG \definecolorxH\OPTcolormodel\OPTcolxH \definecolorxI\OPTcolormodel\OPTcolxI \definecolorxJ\OPTcolormodel\OPTcolxJ \definecolorxK\OPTcolormodel\OPTcolxK \definecolorxL\OPTcolormodel\OPTcolxL \definecolorxM\OPTcolormodel\OPTcolxM

\toprule 𝕊0 𝕊1 𝕊2 𝕊3 𝕊4 𝕊5 𝕊6 𝕊7 𝕊8
\addlinespace[3pt] \midruleπ1 0 \colorboxxG 0 \colorboxxF 0 \colorboxxE 0 \colorboxxD 0 \colorboxxC 0 \colorboxxB 0 \colorboxxA 0
\addlinespace[3pt] π2 0 0 \colorboxxH \colorboxxG 0 \colorboxxF 0 \colorboxxE 0 \colorboxxD 0 \colorboxxC 0 \colorboxxB 0
\addlinespace[3pt] π3 0 0 \colorboxxH \colorboxxG 0 \colorboxxF 0 \colorboxxE 0 \colorboxxD 0 \colorboxxC 0
\addlinespace[3pt] π4 0 0 2 \colorboxxI 2 \colorboxxH \colorboxxG 0 \colorboxxF 0 \colorboxxE 0 \colorboxxD 0
\addlinespace[3pt] π5 0 0 2 2 \colorboxxI 2 \colorboxxH \colorboxxG 0 \colorboxxF 0 \colorboxxE 0
\addlinespace[3pt] π6 0 0 12 12 \colorboxxJ 2 \colorboxxI 2 \colorboxxH \colorboxxG 0 \colorboxxF 0
\addlinespace[3pt] π7 0 0 2 2 ×12 \colorboxxJ 2 \colorboxxI 2 \colorboxxH \colorboxxG 0
\addlinespace[3pt] π8 0 0 2 2 22 \colorboxxK 24 \colorboxxJ 2 \colorboxxI 2 \colorboxxH
\addlinespace[3pt] π9 0 0 3 3 22 2 \colorboxxK 24 \colorboxxJ 2 \colorboxxI 2
\addlinespace[3pt] π10 0 0 15 15 24×3 2 \colorboxxL 0 \colorboxxK 24 \colorboxxJ 2
\addlinespace[3pt] π11 0 0 2 2 15 2 \colorboxxL 0 \colorboxxK 24
\addlinespace[3pt] π12 0 0 22 22 2 30 2 \colorboxxM 0 \colorboxxL 0
\addlinespace[3pt] π13 0 0 12×2 12×2 23 2 60 2 \colorboxxM 0
\addlinespace[3pt] \bottomrule
Table 1: Homotopy groups of spheres [wikipedia-groups]. The kth homotopy group πk of the n-dimensional sphere 𝕊n is isomorphic to the group listed in each entry, where is the additive groupMathworldPlanetmath of integers, and m is the cyclic groupMathworldPlanetmath of order m.

One way of understanding this complexity is through the correspondence between spaces and -groupoids introduced in \crefcha:basics. As discussed in \crefsec:circle, the 2-sphere is presented by a higher inductive type with one point and one 2-dimensional loop. Thus, one might wonder why π3(𝕊2) is , when the type 𝕊2 has no generatorsPlanetmathPlanetmathPlanetmath creating 3-dimensional cells. It turns out that the generating element of π3(𝕊2) is constructed using the interchange law described in the proof of \crefthm:EckmannHilton: the algebraic structure of an -groupoid includes non-trivial interactions between levels, and these interactions create elements of higher homotopy groups.

Type theory provides a natural setting for investigating this structure, as we can easily define the higher homotopy groups. Recall from \crefdef:loopspace that for n:, the n-fold iterated loop space of a pointed type (A,a) is defined recursively by:

Ω0(A,a) =(A,a)
Ωn+1(A,a) =Ωn(Ω(A,a)).

This gives a space (i.e. a type) of n-dimensional loops, which itself has higher homotopies. We obtain the set of n-dimensional loops by truncation (this was also defined as an example in \autorefsec:free-algebras):

Definition 8.0.1 (Homotopy Groups).

Given n1 and (A,a) a pointed type, we define the homotopy groups of A at a by

πn(A,a):Ωn(A,a)0

Since n1, the path concatenation and inversion operations on Ωn(A) induce operations on πn(A) making it into a group in a straightforward way. If n2, then the group πn(A) is abelianMathworldPlanetmath, by the Eckmann–Hilton argument (\autorefthm:EckmannHilton). It is convenient to also write π0(A):A0, but this case behaves somewhat differently: not only is it not a group, it is defined without reference to any basepoint in A.

This definition is a suitable one for investigating homotopy groups because the (higher) inductive definition of a type X presents X as a free type, analogous to a free -groupoid, and this presentation determines but does not explicitly describe the higher identity types of X. The identity types are populated by both the generators (𝗅𝗈𝗈𝗉, for the circle) and the results of applying to them all of the groupoid operations (identity, composition, inversesMathworldPlanetmathPlanetmathPlanetmathPlanetmath, associativity, interchange, …). Thus, the higher-inductive presentation of a space allows us to pose the question “what does the identity type of X really turn out to be?” though it can take some significant mathematics to answer it. This is a higher-dimensional generalizationPlanetmathPlanetmath of a familiar fact in type theory: characterizing the identity type of X can take some work, even if X is an ordinary inductive type, such as the natural numbersMathworldPlanetmath or booleans. For example, the theorem that 0𝟐 is different from 1𝟐 does not follow immediately from the definition; see \autorefsec:compute-coprod.

The univalence axiom plays an essential role in calculating homotopy groups (without univalence, type theory is compatibleMathworldPlanetmath with an interpretation where all paths, including, for example, the loop on the circle, are reflexivityMathworldPlanetmath). We will see this in the calculation of the fundamental group of the circle below: the map from Ω(𝕊1) to is defined by mapping a loop on the circle to an automorphismPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath of the set , so that, for example, 𝗅𝗈𝗈𝗉\centerdot𝗅𝗈𝗈𝗉-1 is sent to 𝗌𝗎𝖼𝖼𝖾𝗌𝗌𝗈𝗋\centerdot𝗉𝗋𝖾𝖽𝖾𝖼𝖾𝗌𝗌𝗈𝗋 (where 𝗌𝗎𝖼𝖼𝖾𝗌𝗌𝗈𝗋 and 𝗉𝗋𝖾𝖽𝖾𝖼𝖾𝗌𝗌𝗈𝗋 are automorphisms of viewed, by univalence, as paths in the universePlanetmathPlanetmath), and then applying the automorphism to 0. Univalence produces non-trivial paths in the universe, and this is used to extract information from paths in higher inductive types.

In this chapter, we first calculate some homotopy groups of spheres, including πk(𝕊1) (\autorefsec:pi1-s1-intro), πk(𝕊n) for k<n (\autorefsec:conn-susp,\autorefsec:pik-le-n), π2(𝕊2) and π3(𝕊2) by way of the Hopf fibration (\autorefsec:hopf) and a long-exact-sequence argument (\autorefsec:long-exact-sequence-homotopy-groups), and πn(𝕊n) by way of the Freudenthal suspension theorem (\autorefsec:freudenthal). Next, we discuss the van Kampen theoremMathworldPlanetmath (\autorefsec:van-kampen), which characterizes the fundamental group of a pushout, and the status of Whitehead’s principle (when is a map that induces an equivalence on all homotopy groups an equivalence?) (\autorefsec:whitehead). Finally, we include brief summaries of additional results that are not included in the book, such as πn+1(𝕊n) for n3, the Blakers–Massey theorem, and a construction of Eilenberg–Mac Lane spaces (\autorefsec:moreresults). Prerequisites for this chapter include \autorefcha:typetheory,\autorefcha:basics,\autorefcha:hits,\autorefcha:hlevels as well as parts of \autorefcha:logic.

Title 8. Homotopy theory
\metatable