Homotopy Type Theory
open problems (Rev #24)

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.

Semantics

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

  • Construct (higher) inductive-recursive types in univalent models, or show that they don’t exist.

  • Connect univalence and parametricity? as suggested here.

  • Show that when the construction of the cumulative hierarchy? in chapter 10 of the book is interpreted in the simplicial set model?, it reproduces (up to equivalence) the usual cumulative hierarchy of the ambient ZFC. Conclude that if HoTT+AC proves that the cumulative hierarchy satisfies some statement of set theory, then that statement follows from ZFC; see also this comment and surrounding discussion.

  • The model invariance problem: show that the interpretation of type theory is independent of the model category? chosen to present an (infinity,1)-category?.

Metatheory

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

  • Is univalence consistent with Induction-Recusion? This would allow us to build a non-univalent universe inside a univalent one.

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

  • Prove or disprove the conjecture that every fibrant type in HTS is equivalent to one definable in MLTT. A potential method of disproof would be to solve the model invariance problem positively for MLTT but negatively for fibrant types in HTS.

Homotopy theory and algebraic topology

  • Similarly to the torus, 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 Segal space? complete Segal space?.

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

Formalization

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

    In general, this file contains a Coq outline of the book. Instructions for how to contribute are here.

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.

  • Prove that the torus? (with the HIT definition involving a 2-dimensional path) is equivalent to a product of two circles. (Sojakova has done this, see here for a proof: Kristina's torus.)

  • 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 May 9, 2014 at 21:49:03 by Alexis Hazell?. See the history of this page for a list of all contributions to it.