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\geq 3$, $\pi_{n+1}(\mathbb{S}^{n})=\mathbb{Z}_{k}$.

###### Notes on the proof..

The proof consists of a calculation of $\pi_{4}(\mathbb{S}^{3})$, together with an appeal to stability (\crefcor: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}(\mathbb{S}^{3})$ is constructive, like all the rest of the proofs in this chapter. (More precisely, it doesn’t use any additional axioms such as $\mathsf{LEM}$ or $\mathsf{AC}$, 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:C\rightarrow X$, and $g:C\rightarrow Y$. Taking first the pushout $X\sqcup^{C}Y$ of $f$ and $g$ and then the pullback of its inclusions ${\mathsf{inl}}:X\rightarrow X\sqcup^{C}Y\leftarrow Y:{\mathsf{inr}}$, we have an induced map $C\to X\times_{(X\sqcup^{C}Y)}Y$.

If $f$ is $i$-connected and $g$ is $j$-connected, then this induced map is $(i+j)$-connected. In other words, for any points $x:X$, $y:Y$, the corresponding fiber $C_{x,y}$ of $(f,g):C\to X\times Y$ gives an approximation to the path space ${\mathsf{inl}}(x)=_{X\sqcup^{C}Y}{\mathsf{inr}}(y)$ 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 (\autorefsec: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(G,n)$ such that $\pi_{n}(K(G,n))=G$, and $\pi_{k}(K(G,n))=0$ for $k\neq 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_{1}(A)$.