Chapter 8 Notes
\topruleTheorem  Status 

\midrule${\pi}_{1}({\mathbb{S}}^{1})$  \ding52\ding52 
$$  \ding52\ding52 
longexactsequence 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 homotopytheoretic theorems that have been proven in homotopy type theory, and whether they have been computerchecked. 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 computerchecked, the principal authors were also the first ones to formalize the proof using a computer proof assistant.

•
Shulman gave the homotopytheoretic calculation of ${\pi}_{1}({\mathbb{S}}^{1})$. Licata later discovered the encodedecode proof and the encodedecode method.

•
Brunerie calculated $$. Licata later gave an encodedecode 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 encodedecode 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:pi1s1homotopytheory, which follows a classical homotopy^{} theoretic one. A typetheoretic analysis of this proof resulted in the development of the encodedecode method. The first calculation of ${\pi}_{2}({\mathbb{S}}^{2})$ also followed classical methods, but this led quickly to an encodedecode proof of the result. The encodedecode calculation generalized to ${\pi}_{n}({\mathbb{S}}^{n})$, which in turn led to the proof of the Freudenthal suspension theorem, by combining an encodedecode argument with classical homotopytheoretic 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 