Chapter 8 Notes

\topruleTheorem Status
\midruleπ1(𝕊1) \ding52\ding52
πk<n(𝕊n) \ding52\ding52
long-exact-sequence of homotopy groupsMathworldPlanetmath \ding52\ding52
total space of Hopf fibration is 𝕊3 \ding52
π2(𝕊2) \ding52\ding52
π3(𝕊2) \ding52
πn(𝕊n) \ding52\ding52
π4(𝕊3) \ding52
Freudenthal suspension theorem \ding52\ding52
Blakers–Massey theorem \ding52\ding52
Eilenberg–Mac Lane spaces K(G,n) \ding52\ding52
van Kampen theoremMathworldPlanetmath \ding52\ding52
covering spaces \ding52\ding52
Whitehead’s principle for n-types \ding52\ding52
Table 1: Theorems from homotopy theory proved by hand (\ding52) and by computer (\ding52\ding52).

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 π1(𝕊1). Licata later discovered the encode-decode proof and the encode-decode method.

  • Brunerie calculated πk<n(𝕊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 𝕊3, thereby calculating π2(𝕊2) and π3(𝕊3).

  • Licata and Brunerie gave a direct calculation of πn(𝕊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 π2(𝕊2), and a calculation of πn(𝕊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 π4(𝕊3).

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

The interplay between homotopy theory and type theoryPlanetmathPlanetmath was crucial to the development of these results. For example, the first proof that π1(𝕊1)= was the one given in \autorefsubsec:pi1s1-homotopy-theory, which follows a classical homotopyMathworldPlanetmath theoretic one. A type-theoretic analysis of this proof resulted in the development of the encode-decode method. The first calculation of π2(𝕊2) also followed classical methods, but this led quickly to an encode-decode proof of the result. The encode-decode calculation generalized to πn(𝕊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 connectionsMathworldPlanetmathPlanetmath between these two subjects.

Title Chapter 8 Notes