Homotopy Type Theory
open problems (Rev #6, changes)

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

Semantics

  • Is there a Quillenmodel 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 amodel 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 ofelementary (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.

Metatheory

  • Give acomputational interpretation?

    Give a computational interpretation? of univalence and HITs.

    of univalence and HITs.
  • Is there acubical 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 themodel of type theory in cubical sets??
  • Show in HoTT that then thn^{th}

    Show in HoTT that the n thn^{th} universe is a model of HoTT with (n1)(n-1) universes.

    universe is a model of HoTT with(n1)(n-1) universes.
  • Consider the type theory with a sequence of universes plus for eachn>0n\gt 0

    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?

    , an axiom asserting that there aren-types? that are not (n1)(n-1)-types. Does adding axioms asserting that each universe is univalent increase the logical strength?

Homotopy theory

  • Prove that thetorus?

    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 theloop 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 morehomotopy groups of spheres

    Calculate more homotopy groups of spheres.

    .
  • Show that thehomotopy 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 3S 7S 4S^3 \to S^7 \to S^4

    Construct the “super Hopf fibration” S 3S 7S 4S^3 \to S^7 \to S^4.

    .

Higher algebra and higher category theory

  • Definesemi-simplicial types?

    Define semi-simplicial types? in type theory.

    in type theory.
  • Define aweak omega-category in type theory?

    Define a weak omega-category in type theory?.

    .

Other mathematics

  • What axioms of set theory are satisfied by theHIT 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 theaxiom 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-inductivereal 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?

Formalization

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

Closed Problems

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!

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