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

Open problems

See open problems

Rough list

• Higher inductive types

• Type families $P : A \to \mathcal{U}$ and fibrations $P(\star_A ) \to \sum_{(a:A)}P(a) \to A$

• homotopy groups of spheres

• pushout $Y \sqcup^X Z$

  • join $X * Y$
  • suspension $\Sigma X$
  • wedge sum $X \vee Y$
  • homotopy fiber
  • homotopy cofiber?
  • smash product $X \wedge Y$

• Eilenberg-MacLane spaces $K(G,n)$

• James construction $J(X) \simeq \Omega \Sigma X$

• localization $L X$

• homology?

• cohomology $H^n(X;A) \equiv \| X \to K(A,n) \|_0$

• spectral sequences

• Hopf construction: H-space on $A$ gives fibration $A \to A * A \to \Sigma A$

• Whitehead product

• loop space of a wedge of circles

• spectrum

• Gysin sequence?

• Hopf invariant?

• Mayer-Vietoris sequence?

• Blakers-Massey Theorem?

• Serre spectral sequence?

• Atiyah–Hirzebruch spectral sequence?

• Seifert-van Kampen theorem

• CW complex?

• Cellular cohomology?

• covering spaces?

Spaces

• circle
• spheres
• interval?
• real projective space?

Useful references

• On the homotopy groups of spheres in homotopy type theory, Guillaume Brunerie

• On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory, Floris van Doorn

• Higher-Dimensional Types in the Mechanization of Homotopy Theory, Favonia

• HoTT book