open problems (Rev #6, changes)

Showing changes from revision #5 to #6:
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?~~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)?

~~(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~~Construct a model of type theory in an (infinity,1)-topos in general.

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

~~out~~~~of~~~~(the~~~~syntactic~~~~category~~~~of)~~~~a~~~~system~~~~of~~~~type~~~~theory.~~~~Define~~~~a~~~~notion~~~~of~~~~elementary (infinity,1)-topos~~Define a notion of elementary (infinity,1)-topos and show that any such admits a model of homotopy type theory.

~~and~~~~show~~~~that~~~~any~~~~such~~~~admits~~~~a~~~~model~~~~of~~~~homotopy~~~~type~~~~theory.~~

~~Give~~~~a~~~~computational interpretation?~~Give a computational interpretation? of univalence and HITs.

~~of~~~~univalence~~~~and~~~~HITs.~~~~Is~~~~there~~~~a~~~~cubical type theory?~~Is there a cubical type theory? that describes more exactly what happens in the model of type theory in cubical sets??

~~that~~~~describes~~~~more~~~~exactly~~~~what~~~~happens~~~~in~~~~the~~~~model of type theory in cubical sets?~~~~?~~~~Show~~~~in~~~~HoTT~~~~that~~~~the~~~~$n^{th}$~~Show in HoTT that the $n^{th}$ universe is a model of HoTT with $(n-1)$ universes.

~~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$~~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?

~~,~~~~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?~~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?)

~~(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~~What is the loop space of a wedge of circles indexed by a set without decidable equality?

~~indexed~~~~by~~~~a~~~~set~~~~without~~~~decidable~~~~equality?~~~~Calculate~~~~more~~~~homotopy groups of spheres~~Calculate more homotopy groups of spheres.

~~.~~~~Show~~~~that~~~~the~~~~homotopy groups of spheres~~Show that the homotopy groups of spheres are all finitely generated, and are finite with the same exceptions as classically.

~~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$~~Construct the “super Hopf fibration” $S^3 \to S^7 \to S^4$.

~~.~~

~~Define~~~~semi-simplicial types?~~Define semi-simplicial types? in type theory.

~~in~~~~type~~~~theory.~~~~Define~~~~a~~~~weak omega-category in type theory?~~Define a weak omega-category in type theory?.

~~.~~

~~What~~~~axioms~~~~of~~~~set~~~~theory~~~~are~~~~satisfied~~~~by~~~~the~~~~HIT model of ZFC?~~What axioms of set theory are satisfied by the HIT model of ZFC? constructed in chapter 10 of the book?

~~constructed~~~~in~~~~chapter~~~~10~~~~of~~~~the~~~~book?~~~~Are~~~~any~~~~of~~~~the~~~~stronger~~~~forms~~~~of~~~~the~~~~axiom of choice?~~Are any of the stronger forms of the axiom of choice? mentioned in the book consistent with univalence?

~~mentioned~~~~in~~~~the~~~~book~~~~consistent~~~~with~~~~univalence?~~~~Do~~~~the~~~~higher~~~~inductive-inductive~~~~real numbers?~~Do the higher inductive-inductive real numbers? from the book coincide with the Escardo-Simpson reals?

~~from~~~~the~~~~book~~~~coincide~~~~with~~~~the~~~~Escardo-Simpson~~~~reals?~~

~~Formalize~~~~the~~~~construction~~~~of~~~~models~~~~of~~~~type~~~~theory~~~~using~~~~contextual~~~~categories.~~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.~~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:?

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.)~~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.)~~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 paper~~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 February 20, 2014 at 10:25:58 by Toby Bartels. See the history of this page for a list of all contributions to it.