# 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}({\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 $\mathrm{\U0001d5ab\U0001d5a4\U0001d5ac}$ or $\mathrm{\U0001d5a0\U0001d5a2}$, 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^{} (\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\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 |
---|---|

\metatable |