8. Homotopy theory

In this chapter, we develop some homotopy theory within type theory. Weuse the synthetic approach to homotopy theory introduced incha:basics: Spaces, points, paths, and homotopies are basicnotions, which are represented by types and elements of types, particularlythe identity type. The algebraic structure of paths and homotopies isrepresented by the natural $\mathrm{\infty }$-groupoidstructure on types, which is generatedby the rules for the identity type. Using higher inductive types, asintroduced in cha:hits, we can describe spaces directly by theiruniversal properties.

There are several interesting aspects of this synthetic approach.First, it combines advantages of concrete models (such as topologicalspacesor simplicial sets)with advantages of abstract categorical frameworksfor homotopy theory (such as Quillen model categories).On the one hand,our proofs feel elementary, and refer concretely topoints, paths, and homotopies in types. On the other hand, our approach nevertheless abstracts away fromany concrete presentation of these objects — for example,associativity of path concatenation is proved by path induction, ratherthan by reparametrization of maps $[0,1]\to X$ or by horn-filling conditions.Type theory seems to be a very convenient way to study the abstract homotopy theoryof $\mathrm{\infty }$-groupoids: by using the rules for the identity type, wecan avoid the complicated combinatorics involved in many definitions of$\mathrm{\infty }$-groupoids, and explicate only as much of thestructure as is needed in any particular proof.

The abstract nature of type theory means that our proofs apply automatically in a variety of settings.In particular, as mentioned previously, homotopy type theory has one interpretation inKan simplicial sets,which is one model for the homotopy theory of $\mathrm{\infty }$-groupoids. Thus,our proofs apply to this model, and transferring them along the geometricrealization functor from simplicial sets to topological spaces givesproofs of corresponding theorems in classical homotopy theory.However, though the details are work in progress, we can alsointerpret type theory in a wide variety of other categoriesthat look like the category of $\mathrm{\infty }$-groupoids, such as$(\mathrm{\infty },1)$-toposes.Thus, proving a result in type theory will showthat 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-theoreticmethods and proofs. Some of our proofs are fairlydirect transcriptions of classical proofs. Others have a moretype-theoretic feel, and consist mainly of calculations with$\mathrm{\infty }$-groupoid operations, in a style that is very similar to howcomputer scientists use type theory to reason about computer programs.One thing that seems to have permitted these new proofs is the fact that type theoryemphasizes different aspects of homotopy theory than other approaches:while tools like path induction and the universal properties of higherinductives are available in a setting like Kan simplicial sets, typetheory elevates their importance, because they are the onlyprimitive tools available for working with these types. Focusing onthese tools had led to new descriptions of familiar constructions suchas the universal cover of the circle and the Hopf fibration, using just therecursion principles for higher inductive types. These descriptions arevery direct, and many of the proofs in this chapter involvecomputational calculations with such fibrations.Another new aspect of our proofs is that they are constructive (assumingunivalence and higher inductives types are constructive); we describe anapplication of this to homotopy groups of spheres insec:moreresults.

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

Before turning to the presentation of our results, we briefly review somebasic concepts and theorems from homotopy theory for the benefit of the reader who is not familiar with them.We also give an overview of theresults 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 questionhomotopy theorists investigate is how to tell whether two spaces are thesame, where “the same” means homotopy equivalence(continuousmaps back and forth that compose to the identity up to homotopy—thisgives the opportunity to “correct” maps that don’t exactly compose tothe identity). One common way to tell whether two spaces are the sameis to calculate algebraic invariants associated with a space,which include its homotopy groups and homology andcohomology groups.Equivalent spaces have isomorphichomotopy/(co)homology groups, so if two spaces have different groups,then they are not equivalent. Thus, these algebraic invariants provideglobal information about a space, which can be used to tell spacesapart, and complements the local information provided by notions such ascontinuity. For example, the torus locally looks like the $2$-sphere, but ithas a global difference, because it as a hole in it, and this differenceis visible in the homotopy groups of these two spaces.

The simplest example of a homotopy group is the fundamental groupof a space, which is written ${\pi }_1(X,x_0$): Given a space $X$ and apoint $x_0$ in it, one can make a group whose elements are loops at$x_0$ (continuous paths from $x_0$ to $x_0$), considered up to homotopy, with thegroup operations given by the identity path (standing still), pathconcatenation, and path reversal. For example, the fundamental group ofthe $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 homotopic to theidentity, because its inside can be filled in. In contrast, a loop onthe torus that goes through the donut’s hole is not homotopic to theidentity, so there are non-trivial elements in the fundamental group.

The higher homotopy groups provide additional information about aspace. Fix a point $x_0$ in $X$, and consider the constant path${\mathrm{𝗋𝖾𝖿𝗅}}_{x_0}$. Then the homotopy classes of homotopies between ${\mathrm{𝗋𝖾𝖿𝗅}}_{x_0}$and itself form a group ${\pi }_2(X,x_0)$, which tells us something aboutthe two-dimensional structure of the space. Then ${\pi }_3(X,x_0$) is thegroup of homotopy classes of homotopies between homotopies, and so on.One of the basic problems of algebraic topology iscalculating the homotopy groups of a space $X$, which meansgiving a group isomorphism between ${\pi }_k(X,x_0)$ and some more directdescription of a group (e.g., by a multiplication table orpresentation). Somewhat surprisingly, this is a very difficultquestion, even for spaces as simple as the spheres. As can be seen fromtab:homotopy-groups-of-spheres, some patterns emerge in thehigher homotopy groups of spheres, but there is no general formula, andmany homotopy groups of spheres are currently still unknown.

xAxBxCxDxExFxGxHxIxJxKxLxM

	${𝕊}^0$	${𝕊}^1$	${𝕊}^2$	${𝕊}^3$	${𝕊}^4$	${𝕊}^5$	${𝕊}^6$	${𝕊}^7$	${𝕊}^8$
[3pt] ${\pi }_1$	$0$	$\mathbb{Z}$	xG $0$	xF $0$	xE $0$	xD $0$	xC $0$	xB $0$	xA $0$
[3pt]${\pi }_2$	$0$	$0$	xH $\mathbb{Z}$	xG $0$	xF $0$	xE $0$	xD $0$	xC $0$	xB $0$
[3pt]${\pi }_3$	$0$	$0$	$\mathbb{Z}$	xH $\mathbb{Z}$	xG $0$	xF $0$	xE $0$	xD $0$	xC $0$
[3pt]${\pi }_4$	$0$	$0$	${\mathbb{Z}}_2$	xI ${\mathbb{Z}}_2$	xH $\mathbb{Z}$	xG $0$	xF $0$	xE $0$	xD $0$
[3pt]${\pi }_5$	$0$	$0$	${\mathbb{Z}}_2$	${\mathbb{Z}}_2$	xI ${\mathbb{Z}}_2$	xH $\mathbb{Z}$	xG $0$	xF $0$	xE $0$
[3pt]${\pi }_6$	$0$	$0$	${\mathbb{Z}}_{12}$	${\mathbb{Z}}_{12}$	xJ ${\mathbb{Z}}_2$	xI ${\mathbb{Z}}_2$	xH $\mathbb{Z}$	xG $0$	xF $0$
[3pt]${\pi }_7$	$0$	$0$	${\mathbb{Z}}_2$	${\mathbb{Z}}_2$	$\mathbb{Z}\times {\mathbb{Z}}_{12}$	xJ ${\mathbb{Z}}_2$	xI ${\mathbb{Z}}_2$	xH $\mathbb{Z}$	xG $0$
[3pt]${\pi }_8$	$0$	$0$	${\mathbb{Z}}_2$	${\mathbb{Z}}_2$	${\mathbb{Z}}_2^2$	xK ${\mathbb{Z}}_{24}$	xJ ${\mathbb{Z}}_2$	xI ${\mathbb{Z}}_2$	xH $\mathbb{Z}$
[3pt]${\pi }_9$	$0$	$0$	${\mathbb{Z}}_3$	${\mathbb{Z}}_3$	${\mathbb{Z}}_2^2$	${\mathbb{Z}}_2$	xK ${\mathbb{Z}}_{24}$	xJ ${\mathbb{Z}}_2$	xI ${\mathbb{Z}}_2$
[3pt]${\pi }_{10}$	$0$	$0$	${\mathbb{Z}}_{15}$	${\mathbb{Z}}_{15}$	${\mathbb{Z}}_{24}\times {\mathbb{Z}}_3$	${\mathbb{Z}}_2$	xL $0$	xK ${\mathbb{Z}}_{24}$	xJ ${\mathbb{Z}}_2$
[3pt]${\pi }_{11}$	$0$	$0$	${\mathbb{Z}}_2$	${\mathbb{Z}}_2$	${\mathbb{Z}}_{15}$	${\mathbb{Z}}_2$	$\mathbb{Z}$	xL $0$	xK ${\mathbb{Z}}_{24}$
[3pt]${\pi }_{12}$	$0$	$0$	${\mathbb{Z}}_2^2$	${\mathbb{Z}}_2^2$	${\mathbb{Z}}_2$	${\mathbb{Z}}_{30}$	${\mathbb{Z}}_2$	xM $0$	xL $0$
[3pt]${\pi }_{13}$	$0$	$0$	${\mathbb{Z}}_{12}\times {\mathbb{Z}}_2$	${\mathbb{Z}}_{12}\times {\mathbb{Z}}_2$	${\mathbb{Z}}_2^3$	${\mathbb{Z}}_2$	${\mathbb{Z}}_{60}$	${\mathbb{Z}}_2$	xM $0$
[3pt]

Table 1: Homotopy groups of spheres [wikipedia-groups].The $k^{\text{th}}$ homotopy group ${\pi }_k$ of the $n$-dimensional sphere${𝕊}^n$ is isomorphic to the group listed in each entry, where $\mathbb{Z}$ isthe additive group of integers, and ${\mathbb{Z}}_m$ is the cyclic group of order $m$.

One way of understanding this complexity is through the correspondencebetween spaces and $\mathrm{\infty }$-groupoidsintroduced in cha:basics.As discussed in sec:circle, the 2-sphere is presented by a higherinductive type with one point and one 2-dimensional loop. Thus, onemight wonder why ${\pi }_3({𝕊}^2)$ is $\mathbb{Z}$, when the type ${𝕊}^2$ has nogenerators creating 3-dimensional cells. It turns out that thegenerating element of ${\pi }_3({𝕊}^2)$ is constructed using theinterchange law described in the proof of thm:EckmannHilton: thealgebraic structure of an $\mathrm{\infty }$-groupoid includes non-trivialinteractions between levels, and these interactions create elements ofhigher homotopy groups.

Type theory provides a natural setting for investigating this structure, aswe can easily define the higher homotopy groups. Recall from def:loopspace that for $n:\mathbb{N}$, the$n$-fold iterated loop space of a pointed type $(A,a)$ is definedrecursively by:

${\mathrm{\Omega }}^0(A,a)$$=(A,a)$

${\mathrm{\Omega }}^{n+1}(A,a)$$={\mathrm{\Omega }}^n(\mathrm{\Omega }(A,a)).$

This gives a space (i.e. a type) of $n$-dimensional loops, which itself hashigher homotopies. We obtain the set of $n$-dimensional loops bytruncation (this was also defined as an example insec:free-algebras):

Definition 8.0.1 (Homotopy Groups).

Given $n\mathrm{\ge }\mathrm{1}$ and $\mathrm{(}A\mathrm{,}a\mathrm{)}$ a pointed type, we define the homotopy groups of $A$at $a$ by

$${\pi }_n(A,a):\equiv {\parallel {\mathrm{\Omega }}^n(A,a)\parallel }_0$$

Since $n\ge 1$, the path concatenation and inversion operations on${\mathrm{\Omega }}^n(A)$ induce operations on ${\pi }_n(A)$ making it into a group ina straightforward way. If $n\ge 2$, then the group ${\pi }_n(A)$ isabelian, by the Eckmann–Hilton argument (thm:EckmannHilton).It is convenient to also write ${\pi }_0(A):\equiv \parallel A{\parallel }_0$,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 groupsbecause the (higher) inductive definition of a type $X$ presents $X$ asa free type, analogous to a free $\mathrm{\infty }$-groupoid,and thispresentation determines but does not explicitly describethe higher identity types of $X$. The identity types are populated byboth the generators ($\mathrm{𝗅𝗈𝗈𝗉}$, for the circle) and the results of applying to them all of the groupoidoperations (identity, composition, inverses, associativity, interchange,…). Thus, the higher-inductive presentation of a space allows usto pose the question “what does the identity type of $X$ really turn outto be?” though it can take some significant mathematics to answer it.This is a higher-dimensional generalization of a familiar fact in typetheory: characterizing the identity type of $X$ can take some work,even if $X$ is an ordinary inductive type, such as the natural numbersor booleans. For example, the theorem that $0_{\mathrm{𝟐}}$ is differentfrom $1_{\mathrm{𝟐}}$ does not follow immediately from the definition;see sec:compute-coprod.

The univalence axiom plays an essential role in calculating homotopygroups (without univalence, type theory is compatible with aninterpretation where all paths, including, for example, the loop on thecircle, are reflexivity). We will see this in the calculation of thefundamental group of the circle below: the map from $\mathrm{\Omega }({𝕊}^1)$ to $\mathbb{Z}$ is defined by mapping a loop on the circle to anautomorphism of the set $\mathbb{Z}$, so that, for example, $\mathrm{𝗅𝗈𝗈𝗉}{\mathrm{𝗅𝗈𝗈𝗉}}^{-1}$ is sent to $\mathrm{𝗌𝗎𝖼𝖼𝖾𝗌𝗌𝗈𝗋}\mathrm{𝗉𝗋𝖾𝖽𝖾𝖼𝖾𝗌𝗌𝗈𝗋}$ (where$\mathrm{𝗌𝗎𝖼𝖼𝖾𝗌𝗌𝗈𝗋}$ and $\mathrm{𝗉𝗋𝖾𝖽𝖾𝖼𝖾𝗌𝗌𝗈𝗋}$ are automorphisms of$\mathbb{Z}$ viewed, by univalence, as paths in the universe), and then applyingthe automorphism to 0. Univalence produces non-trivial paths in theuniverse, and this is used to extract information from paths in higherinductive types.

In this chapter, we first calculate some homotopy groups of spheres,including ${\pi }_k({𝕊}^1)$ (sec:pi1-s1-intro), ${\pi }_k({𝕊}^n)$ for (sec:conn-susp,sec:pik-le-n), ${\pi }_2({𝕊}^2)$ and ${\pi }_3({𝕊}^2)$ byway of the Hopf fibration (sec:hopf) and a long-exact-sequenceargument (sec:long-exact-sequence-homotopy-groups), and${\pi }_n({𝕊}^n)$ by way of the Freudenthal suspension theorem(sec:freudenthal). Next, we discuss the van Kampen theorem(sec:van-kampen), which characterizes the fundamental group ofa pushout, and the status of Whitehead’s principle (when is a map thatinduces an equivalence on all homotopy groups an equivalence?)(sec:whitehead). Finally, we include brief summaries ofadditional results that are not included in the book, such as${\pi }_{n+1}({𝕊}^n)$ for $n\ge 3$, the Blakers–Massey theorem, and aconstruction of Eilenberg–Mac Lane spaces (sec:moreresults).Prerequisites for this chapter include cha:typetheory,cha:basics,cha:hits,cha:hlevels as well as parts of cha:logic.