# Homotopy Type Theory Synthetic homotopy theory (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

## 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

## Closed Problems

• 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$.

## Useful references

Revision on August 18, 2018 at 08:40:40 by Ali Caglayan. See the history of this page for a list of all contributions to it.