Homotopy Type Theory
open problems (Rev #15, changes)

Showing changes from revision #14 to #15: Added | Removed | Changed

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.


  • Is there a Quillen model structure on semi-simplicial sets? (with semi-simplicial Kan fibrations) making it Quillen equivalent to simplicial sets (with Kan fibrations)? (Is this a solution?)

  • Construct a model of type theory in an (infinity,1)-topos in general.

  • Construct an (infinity,1)-topos? out of (the syntactic category of) a system of type theory.

  • Define a notion of elementary (infinity,1)-topos and show that any such admits a model of homotopy type theory.

  • Semantics for strict resizing

  • Semantics for Higher inductive recursive types.

  • Connect univalence and parametricity as suggested here.


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

  • What is the proof theoretic strength of univalent type theory plus HITs? In particular, can they be predicatively justified?

  • Consider Is the univalence type consistent theory with Induction-Recusion? This would allow us to build a sequence non-univalent of universe universes inside plus a for univalent each one.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?

  • 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 and algebraic topology

  • Prove that the torus? (with the HIT definition involving a 2-dimensional path) is equivalent to a product of two circles. (Kristina has done this. Formalization seems difficult.) Similarly, consider the projective plane, Klein bottle, … as discussed in the book.

  • 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 fibrationS 3S 7S 4S^3 \to S^7 \to S^4.

  • Define the Whitehead product.

  • Define the Toda bracket.

  • Prove that nn-spheres are \infty-truncated.

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

  • Can we verify computational algebraic topology using HoTT?

  • Bott periodicity

  • Develop synthetic stable homotopy theory

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? For instance, does it satisfy collection or REA?

  • 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 Semi-simplicial types.

  • Formalize \infty-groupoids, \infty-categories within HoTT.

  • Formalize what remains to be done from chapters 8, 10, and 11 of the book. In particular, develop Higher Inductive Inductive Types in Coq.

Closed problems

How about keeping a running list of solutions like this:?

Maybe only things not in the HoTT book? Else the list of solved problems gets very long!

OK, here’s the rule: if it was stated here (or on the UF-wiki) as an open problem, then it gets recorded here once it’s solved.

  • Construct the Hopf fibration. (Lumsdaine gave the construction in 2012 and Brunerie proved it was correct in 2013.)

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

Revision on March 5, 2014 at 09:30:00 by Bas Spitters. See the history of this page for a list of all contributions to it.