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 nn-spheres are \infty-truncated.

  • Prove that S 2S^2 is not an nn-type.

  • Define the/a delooping of S 3S^3.

  • Can we verify computational algebraic topology using HoTT?

  • Bott periodicity

  • Develop synthetic stable homotopy theory

See open problems

Closed Problems

Useful constructions

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.