Chapter 8 Notes

Theorem	Status
${\pi }_1({𝕊}^1)$	5252
	5252
long-exact-sequence of homotopy groups	5252
total space of Hopf fibration is ${𝕊}^3$	52
${\pi }_2({𝕊}^2)$	5252
${\pi }_3({𝕊}^2)$	52
${\pi }_n({𝕊}^n)$	5252
${\pi }_4({𝕊}^3)$	52
Freudenthal suspension theorem	5252
Blakers–Massey theorem	5252
Eilenberg–Mac Lane spaces $K(G,n)$	5252
van Kampen theorem	5252
covering spaces	5252
Whitehead’s principle for $n$-types	5252

Table 1: Theorems from homotopy theory proved byhand (52) and by computer (5252).

The theorems described in this chapter are standard results in classicalhomotopy theory; many are described by [hatcher02topology]. In thesenotes, we review the development of the new synthetic proofs of them in homotopytype theory. tab:theorems lists the homotopy-theoretictheorems that have been proven in homotopy type theory, and whether theyhave been computer-checked.Almost all of these results were developed during the spring term at IASin 2013, as part of a significant collaborative effort. Many peoplecontributed to these results, for example by being the principal authorof a proof, by suggesting problems to work on, by participating in manydiscussions and seminars about these problems, or by giving feedback onresults. The following people were the principal authors of the firsthomotopy type theory proofs of the above theorems. Unless indicated otherwise, for thetheorems that have been computer-checked, the principal authors werealso the first ones to formalize the proof using a computer proofassistant.

• Shulman gave the homotopy-theoretic calculation of ${\pi }_1({𝕊}^1)$. Licata later discovered theencode-decode proof and the encode-decode method.

• Brunerie calculated .Licata later gave an encode-decode version.

• Voevodsky constructed the long exact sequence of homotopy groups.

• Lumsdaine constructed the Hopf fibration.Brunerie proved that its total space is ${𝕊}^3$, thereby calculating ${\pi }_2({𝕊}^2)$ and${\pi }_3({𝕊}^3)$.

• Licata and Brunerie gave a direct calculation of${\pi }_n({𝕊}^n)$.

• Lumsdaine proved the Freudenthal suspension theorem; Licata andLumsdaine formalized this proof.

• Lumsdaine, Finster, and Licata proved the Blakers–Massey theorem;Lumsdaine, Brunerie, Licata, and Hou formalized it.

• Licata gave an encode-decode calculation of ${\pi }_2({𝕊}^2)$, and acalculation of ${\pi }_n({𝕊}^n)$ using the Freudenthal suspension theorem; using similartechniques, he constructed $K(G,n)$.

• Shulman proved the van Kampen theorem; Hou formalized this proof.

• Licata proved Whitehead’s theorem for $n$-types.

• Brunerie calculated ${\pi }_4({𝕊}^3)$.

• Hou established the theory of covering spaces and formalized it.

The interplay between homotopy theory and type theory was crucial to thedevelopment of these results. For example, the first proof that${\pi }_1({𝕊}^1)=\mathbb{Z}$ was the one given in subsec:pi1s1-homotopy-theory, which follows a classical homotopy theoretic one. Atype-theoretic analysis of this proof resulted in the development of theencode-decode method. The first calculation of ${\pi }_2({𝕊}^2)$ also followedclassical methods, but this led quickly to an encode-decode proof of theresult. The encode-decode calculation generalized to ${\pi }_n({𝕊}^n)$, whichin turn led to the proof of the Freudenthal suspension theorem, bycombining an encode-decode argument with classical homotopy-theoreticreasoning about connectedness, which in turn led to the Blakers–Masseytheorem and Eilenberg–Mac Lane spaces. The rapid development of thisseries of results illustrates the promise of our new understanding ofthe connections between these two subjects.