Showing changes from revision #1 to #2:
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)?
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 universe is a model of HoTT with universes.
Consider the type theory with a sequence of universes plus for each , an axiom asserting that there are n-types? that are not -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.