The following is a list of topics and results of homotopy theory that have been formalized in homotopy type theory.
On homotopy groups of spheres:
Dan’s construction.
$K(G,n)$ is a spectrum, formalized
Cohomology of the n-torus, which could be easily extended to any finite product of spheres.
to do:
cohomology with finite coefficients, all we need is the boring work of defining $\mathbb{Z}/p\mathbb{Z}$ as an explicit group.
Calculate some more cohomology groups.
Compute the loop space of this construction and use it to define spectra.
On the Freudenthal suspension theorem:
Implies $\pi_k(S^n) = \pi_{k+1}(S^{n+1})$ whenever $k \leq 2n - 2$
Peter’s encode/decode-style proof, formalized by Dan, using a clever lemma about maps out of 2 n-connected types. This is the “95%” version, which shows that the relevant map is an equivalence on truncations.
The full “100%” version, formalized by Dan, which shows that the relevant map is $2n$-connected.
On homotopy limits:
On the van Kampen theorem:
On covering spaces:
Created on June 9, 2022 at 07:13:54. See the history of this page for a list of all contributions to it.