UF IAS 2012 Archive
Formalized Homotopy Theory

Here are some links to proofs about homotopy theory, formalized in homotopy type theory. Please add!

Cast of characters so far: Jeremy Avigad, Guillaume Brunerie, Favonia, Eric Finster, Chris Kapulkin, Dan Licata, Peter Lumsdaine, Mike Shulman.

In progress

π4(S3)

π3(S2)

Cohomology

At least one proof has been formalized

Whitehead’s theorem

K(G,n)

Freudenthal Suspension Theorem

Implies π_k(Sn) = π_k+1(Sn+1) whenever k <= 2n - 2

π_n(Sn)

π_k(Sn) for k < n

π2(S2)

π1(S1)

A paper mostly about the encode/decode-style proof, but also describing the relationship between the two.

Homotopy limits

Van Kampen

Covering spaces

Blakers-Massey

Created on April 19, 2018 at 17:16:58 by Univalent foundations special year 2012