Homotopy Type Theory
open problems (Rev #1)

A list of (believed to be) open problems in homotopy type theory. To add more detail about a problem (such as why it is hard or interesting, or what ideas have been tried), make a link to a new page.



  • Give a computational interpretation? of univalence and HITs.
  • Is there a cubical type theory? that describes more exactly what happens in the model of type theory in cubical sets??
  • Show in HoTT that the n thn^{th} universe is a model of HoTT with (n1)(n-1) universes.
  • Consider the type theory with a sequence of universes plus for each n>0n\gt 0, an axiom asserting that there are n-types? that are not (n1)(n-1)-types. Does adding axioms asserting that each universe is univalent increase the logical strength?

Homotopy theory

  • Prove that the torus? (with the HIT definition involving a 2-dimensional path) is equivalent to a product of two circles.
  • 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.
  • Construct the “super Hopf fibration” S 3S 7S 4S^3 \to S^7 \to S^4.

Higher algebra and higher category theory

  • Define semi-simplicial types? in type theory.
  • Define a weak omega-category in type theory?.

Other Mathematics

  • What axioms of set theory are satisfied by the HIT model of ZFC? constructed in chapter 10 of the book?
  • Are any of the stronger forms of the axiom of choice? mentioned in the book consistent with univalence?
  • Do the higher inductive-inductive real numbers? from the book coincide with the Escardo-Simpson reals?


  • Formalize the construction of models of type theory using contextual categories.
  • Formalize what remains to be done from chapters 8, 10, and 11 of the book.

Revision on February 18, 2014 at 13:08:19 by Mike Shulman. See the history of this page for a list of all contributions to it.