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. * table of contents {: toc} ## Semantics * Is there a Quillen [[nLab:model structure on semi-simplicial sets]] (with semi-simplicial Kan fibrations) making it Quillen equivalent to simplicial sets (with Kan fibrations)? * Construct a [[model of type theory in an (infinity,1)-topos]] in general. * Construct an [[nLab:(infinity,1)-topos]] out of (the syntactic category of) a system of type theory. * Define a notion of [[nLab:elementary (infinity,1)-topos]] and show that any such admits a model of homotopy type theory. ## 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^{th}$ universe is a model of HoTT with $(n-1)$ universes. * Consider the type theory with a sequence of universes plus for each $n\gt 0$, an axiom asserting that there are [[n-type|n-types]] that are not $(n-1)$-types. Does adding axioms asserting that each universe is [[univalence|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. (Has Kristina done this?) * What is the [[loop space of a wedge of circles]] indexed by a set without decidable equality? * Calculate more [[nLab:homotopy groups of spheres]]. * Show that the [[nLab:homotopy groups of spheres]] are all finitely generated, and are finite with the same exceptions as classically. * Construct the "super Hopf fibration" $S^3 \to S^7 \to S^4$. * Define the Whitehead product. * Define the Toda bracket. ## Higher algebra and higher category theory * Define [[nLab:semi-simplicial type|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? ## Formalization * 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. ## Closed problems +-- {: .query} 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! =-- * Construct the Hopf fibration. (Lumsdaine gave the construction in 2012 and Brunerie proved it was correct in 2013.) * Prove the [[nLab: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](http://dlicata.web.wesleyan.edu/pubs/lf14em/lf14em.pdf) (pdf).)