open problems (Rev #3, changes)

Showing changes from revision #2 to #3:
Added | ~~Removed~~ | ~~Chan~~ged

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

- 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-types? that are not $(n-1)$-types. Does adding axioms asserting that each universe is univalent increase the logical strength?

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

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

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

- Construct the Hopf fibration. (Lumsdaine gave the construction in 2012 and Brunerie proved it was correct in 2013.)
- Prove the Siefert-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 paperhe link).)