Homotopy Type Theory Synthetic homotopy theory > history (Rev #1)

Open problems

Similarly to the torus, consider the projective plane, Klein bottle, … as discussed in the book (sec 6.6). Show that the Klein bottle is not orientable. (This requires defining “orientable”.)
What is the loop space of a wedge of circles indexed by a set without decidable equality?
Calculate more homotopy groups of spheres.
Show that the homotopy groups of spheres are all finitely generated, and are finite with the same exceptions as classically.
Define the Toda bracket.
Prove that $n$ -spheres are $\infty$ -truncated.
Prove that $S^2$ is not an $n$ -type.
Define the/a delooping of $S^3$ .
Can we verify computational algebraic topology using HoTT?
Bott periodicity
Develop synthetic stable homotopy theory

Prove that the torus? (with the HIT definition involving a 2-dimensional path) is equivalent to a product of two circles. See Sojakova’s proof: Kristina's torus. A shorter formalized proof is here
Construct the Hopf fibration. (Lumsdaine gave the construction in 2012 and Brunerie proved it was correct in 2013.)
Construct the “super Hopf fibration” (AKA quaternionic Hopf fibration) $S^3 \to S^7 \to S^4$ . (Buchholtz and Rijke solved this early 2016 through a homotopy version of the Cayley-Dickson construction.)
Prove the Seifert-van Kampen theorem. (Shulman did it in 2013.)
Construct Eilenberg-MacLane spaces and use them to define cohomology. (Licata and Finster did it in 2013, written up in this paper (pdf).)
Define the Whitehead product. Guillaume Brunerie did this in 2017, written up in this paper. he also gives a constructive proof of $\pi_4( S^3)= Z/n Z$ for some $n$ and a construction of the James construction (reduced James product) as a HIT and a homotopy colimit. It is also proven that $\Omega \Sigma X \simeq J(X)$ for some pointed connected type $X$ .

Revision on August 5, 2018 at 13:47:58 by Ali Caglayan. See the history of this page for a list of all contributions to it.