8.10 Additional Results
Though we do not present the proofs in this chapter, following results have also been established in homotopy type theory.
There exists a such that for all , .
Notes on the proof..
The proof consists of a calculation of , together with an appeal to stability (\crefcor:stability-spheres). In the classical statement of this result, is . While we have not yet checked that is in fact , our calcluation of is constructive, like all the rest of the proofs in this chapter. (More precisely, it doesn’t use any additional axioms such as or , 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 is . 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).
It should be noted that in classical algebraic topology, the Blakers–Massey theorem is often stated in a somewhat different form, where the maps and 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 and positive integer , there is an -type such that , and for .
Theorem 8.10.4 (Covering spaces).
For a connected space , there is an equivalence between covering spaces over and sets with an action of .
|Title||8.10 Additional Results|