[[!redirects Open problems]] [[!redirects open problems]] 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 [[model structure on semi-simplicial sets]] (with semi-simplicial Kan fibrations) making it Quillen equivalent to simplicial sets (with Kan fibrations)? (Is [this](http://uf-ias-2012.wikispaces.com/file/view/semisimplicialsets.pdf/421930564/semisimplicialsets.pdf) a solution?) * 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. * [[Semantics]] for strict [[resizing rules]]. * Construct (higher) [[inductive-recursive type|inductive-recursive types]] in univalent models, or show that they don't exist. * Connect [[univalence]] and [[parametricity]] as suggested [here](http://bentnib.org/dtt-parametricity.pdf). * Show that when the construction of the [[cumulative hierarchy]] in chapter 10 of the book is interpreted in the [[simplicial set model]], it reproduces (up to equivalence) the usual cumulative hierarchy of the ambient ZFC. Conclude that if HoTT+AC proves that the cumulative hierarchy satisfies some statement of set theory, then that statement follows from ZFC; see also [this comment](http://math.andrej.com/2014/01/13/univalent-foundations-subsume-classical-mathematics/comment-page-1/#comment-34342) and surrounding discussion. * The [[model invariance problem]]: show that the interpretation of type theory is independent of the [[model category]] chosen to present an [[(infinity,1)-category]]. ## Metatheory * "Writing all inductive definitions in terms of Sigma-types and W-types is theoretically possible, but extremely tedious ... it’s unknown whether any similar reduction for HITs is possible." ([source](http://homotopytypetheory.org/2014/06/08/hiru-tdd/)) * 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. * What is the proof theoretic strength of univalent type theory plus HITs? In particular, can they be predicatively justified? [Strength of MLTT+W](http://cs-svr1.swan.ac.uk/~csetzer/articles/weor0.pdf) * Is univalence consistent with Induction-Recusion? This would allow us to build a non-univalent universe inside a univalent one. Related to this, higher inductive types [can](http://homotopytypetheory.org/2014/06/08/hiru-tdd/) be used to define a univalent universe. * 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? * Prove or disprove the conjecture that every fibrant type in [[HTS]] is equivalent to one definable in [[Martin-Löf Type Theory|MLTT]]. A potential method of disproof would be to solve the [[model invariance problem]] positively for MLTT but negatively for fibrant types in HTS. ## Homotopy theory and algebraic topology * Similarly to the torus, consider the projective plane, Klein bottle, ... as discussed in the book. * 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$. * Define the Whitehead product. * Define the Toda bracket. * Prove that $n$-spheres are $\infty$-truncated. * Prove that $S^2$ is not an $n$-type. * Can we verify [computational algebraic topology](http://www-fourier.ujf-grenoble.fr/~sergerar/Kenzo/) using HoTT? * Bott periodicity * Develop synthetic stable homotopy theory ## Higher algebra and higher category theory * Define [[semi-simplicial type|semi-simplicial types]] in type theory. Define [[Segal space]] [[complete Segal space]]. * Define a [[weak omega-category in type theory]]. * Is it possible to have limits be judgmentally the same as opposite colimits, and simultaneously have (co)limits be judgmentally the same as particular Kan extensions. As partially detailed [on an issue on the HoTT/HoTT repo](https://github.com/HoTT/HoTT/issues/284), part of the problem is that the functor ᵒᵖ : (D → C)ᵒᵖ → (Dᵒᵖ → Cᵒᵖ) has a judgmental inverse (the composition is judgmentally the identity functor on objects and morphisms), and, assuming univalence, the precategories (D → C)ᵒᵖ and (Dᵒᵖ → Cᵒᵖ) are propositionally but not judgmentally equal. ## Other mathematics * What axioms of set theory are satisfied by the [[HIT model of ZFC]] constructed in chapter 10 of the book? For instance, does it satisfy collection or REA? * 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 [[semi-simplicial types]]. * Formalize $\infty$-groupoids, $\infty$-categories within HoTT. * Formalize what remains to be done from chapters 8, 10, and 11 of the book. In particular, develop Higher Inductive Inductive Types in Coq. In general, [this file](https://github.com/HoTT/HoTT/blob/master/contrib/HoTTBook.v) contains a Coq outline of the book. Instructions for how to contribute are [here](https://github.com/HoTT/HoTT/blob/master/README.markdown). ## 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! OK, here's the rule: if it was stated here (or on the UF-wiki) as an open problem, then it gets recorded here once it's solved. =-- * Prove that the [[torus]] (with the HIT definition involving a 2-dimensional path) is equivalent to a product of two circles. (Sojakova has done this, see here for a proof: [[torus.pdf:file]].) * Construct the Hopf fibration. (Lumsdaine gave the construction in 2012 and Brunerie proved it was correct in 2013.) * Prove the [[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).)