Chapter 8 Notes

Mathworld — Table 1: Theorems from homotopy theory proved by hand (\ding52) and by computer (\ding52\ding52).

\topruleTheorem	Status
\midrule $\pi_{1}(\mathbb{S}^{1})$	\ding52\ding52
$\pi_{k<n}(\mathbb{S}^{n})$	\ding52\ding52
long-exact-sequence of homotopy groups	\ding52\ding52
total space of Hopf fibration is $\mathbb{S}^{3}$	\ding52
$\pi_{2}(\mathbb{S}^{2})$	\ding52\ding52
$\pi_{3}(\mathbb{S}^{2})$	\ding52
$\pi_{n}(\mathbb{S}^{n})$	\ding52\ding52
$\pi_{4}(\mathbb{S}^{3})$	\ding52
Freudenthal suspension theorem	\ding52\ding52
Blakers–Massey theorem	\ding52\ding52
Eilenberg–Mac Lane spaces $K(G,n)$	\ding52\ding52
van Kampen theorem	\ding52\ding52
covering spaces	\ding52\ding52
Whitehead’s principle for $n$ -types	\ding52\ding52
\bottomrule

The theorems described in this chapter are standard results in classical homotopy theory; many are described by [hatcher02topology]. In these notes, we review the development of the new synthetic proofs of them in homotopy type theory. \autoreftab:theorems lists the homotopy-theoretic theorems that have been proven in homotopy type theory, and whether they have been computer-checked. Almost all of these results were developed during the spring term at IAS in 2013, as part of a significant collaborative effort. Many people contributed to these results, for example by being the principal author of a proof, by suggesting problems to work on, by participating in many discussions and seminars about these problems, or by giving feedback on results. The following people were the principal authors of the first homotopy type theory proofs of the above theorems. Unless indicated otherwise, for the theorems that have been computer-checked, the principal authors were also the first ones to formalize the proof using a computer proof assistant.

•

Shulman gave the homotopy-theoretic calculation of $\pi_{1}(\mathbb{S}^{1})$ . Licata later discovered the encode-decode proof and the encode-decode method.
•

Brunerie calculated $\pi_{k<n}(\mathbb{S}^{n})$ . 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 $\mathbb{S}^{3}$ , thereby calculating $\pi_{2}(\mathbb{S}^{2})$ and $\pi_{3}(\mathbb{S}^{3})$ .
•

Licata and Brunerie gave a direct calculation of $\pi_{n}(\mathbb{S}^{n})$ .
•

Lumsdaine proved the Freudenthal suspension theorem; Licata and Lumsdaine 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}(\mathbb{S}^{2})$ , and a calculation of $\pi_{n}(\mathbb{S}^{n})$ using the Freudenthal suspension theorem; using similar techniques, 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}(\mathbb{S}^{3})$ .
•

Hou established the theory of covering spaces and formalized it.

The interplay between homotopy theory and type theory was crucial to the development of these results. For example, the first proof that $\pi_{1}(\mathbb{S}^{1})=\mathbb{Z}$ was the one given in \autorefsubsec:pi1s1-homotopy-theory, which follows a classical homotopy theoretic one. A type-theoretic analysis of this proof resulted in the development of the encode-decode method. The first calculation of $\pi_{2}(\mathbb{S}^{2})$ also followed classical methods, but this led quickly to an encode-decode proof of the result. The encode-decode calculation generalized to $\pi_{n}(\mathbb{S}^{n})$ , which in turn led to the proof of the Freudenthal suspension theorem, by combining an encode-decode argument with classical homotopy-theoretic reasoning about connectedness, which in turn led to the Blakers–Massey theorem and Eilenberg–Mac Lane spaces. The rapid development of this series of results illustrates the promise of our new understanding of the connections between these two subjects.

Title	Chapter 8 Notes
\metatable