8.10 Additional Results

Though we do not present the proofs in this chapter, following results have also been established in homotopy type theory.

Theorem 8.10.1.

There exists a $k$ such that for all $n\mathrm{\ge }\mathrm{3}$, ${\pi }_{n\mathrm{+}\mathrm{1}}\mathit{}\mathrm{(}{\mathrm{S}}^n\mathrm{)}\mathrm{=}{\mathrm{Z}}_k$.

Notes on the proof..

The proof consists of a calculation of ${\pi }_4({𝕊}^3)$, together with an appeal to stability (cor:stability-spheres). In the classical statement of this result, $k$ is $2$. While we have not yet checked that $k$ is in fact $2$, our calcluation of ${\pi }_4({𝕊}^3)$ is constructive, like all the rest of the proofs in this chapter. (More precisely, it doesn’t use any additional axioms such as $\mathrm{𝖫𝖤𝖬}$ or $\mathrm{𝖠𝖢}$, making it as constructive as univalence and higher inductive types are.) Thus, given a computational interpretation of homotopy type theory, we could run the proof on a computer to verify that $k$ is $2$. This example is quite intriguing, because it is the first calculation of a homotopy group for which we have not needed to know the answer in advance. ∎

Theorem 8.10.2 (Blakers–Massey theorem).

Suppose we are given maps $f\mathrm{:}C\mathrm{\to }X$, and $g\mathrm{:}C\mathrm{\to }Y$. Taking first the pushout $X{\mathrm{\bigsqcup }}^{C}Y$ of $f$ and $g$ and then the pullback of its inclusions $\mathrm{inl}\mathrm{:}X\mathrm{\to }X{\mathrm{\bigsqcup }}^{C}Y\mathrm{\leftarrow }Y\mathrm{:}\mathrm{inr}$, we have an induced map $C\mathrm{\to }X{\mathrm{\times }}_{\mathrm{(}X{\mathrm{\bigsqcup }}^{C}Y\mathrm{)}}Y$.

If $f$ is $i$-connected and $g$ is $j$-connected, then this induced map is $\mathrm{(}i\mathrm{+}j\mathrm{)}$-connected. In other words, for any points $x\mathrm{:}X$, $y\mathrm{:}Y$, the corresponding fiber $C_{x\mathrm{,}y}$ of $\mathrm{(}f\mathrm{,}g\mathrm{)}\mathrm{:}C\mathrm{\to }X\mathrm{\times }Y$ gives an approximation to the path space $\mathrm{inl}\mathit{}\mathrm{(}x\mathrm{)}{\mathrm{=}}_{X{\mathrm{\bigsqcup }}^{C}Y}\mathrm{inr}\mathit{}\mathrm{(}y\mathrm{)}$ in the pushout.

It should be noted that in classical algebraic topology, the Blakers–Massey theorem is often stated in a somewhat different form, where the maps $f$ and $g$ are replaced by inclusions of subcomplexes of CW complexes, and the homotopy pushout and homotopy pullback by a union and intersection, respectively. In order to express the theorem in homotopy type theory, we have to replace notions of this sort with ones that are homotopy-invariant. We have seen another example of this in the van Kampen theorem (sec:van-kampen), where we had to replace a union of open subsets by a homotopy pushout.

Theorem 8.10.3 (Eilenberg–Mac Lane Spaces).

For any abelian group $G$ and positive integer $n$, there is an $n$-type $K\mathit{}\mathrm{(}G\mathrm{,}n\mathrm{)}$ such that ${\pi }_n\mathit{}\mathrm{(}K\mathit{}\mathrm{(}G\mathrm{,}n\mathrm{)}\mathrm{)}\mathrm{=}G$, and ${\pi }_k\mathit{}\mathrm{(}K\mathit{}\mathrm{(}G\mathrm{,}n\mathrm{)}\mathrm{)}\mathrm{=}\mathrm{0}$ for $k\mathrm{\ne }n$.

Theorem 8.10.4 (Covering spaces).

For a connected space $A$, there is an equivalence between covering spaces over $A$ and sets with an action of ${\pi }_{\mathrm{1}}\mathit{}\mathrm{(}A\mathrm{)}$.

Title	8.10 Additional Results