Homotopy Type Theory
HoTT2019 Summer School open problems list (Rev #2)

Here are the open problems stated at the HoTT 2019 Summer School, listed by the instructor who posed the problem:

Mathieu Anel: Logos Theory

  • notion of higher theory? (CAT^lex, CAT_cc, LOGOS, …)

  • distributivity in Logoi colim lim —> lim colim, polynomial calculus

  • define Sym: CAT_cc —> LOGOI

  • internal cat theory in a logos

  • define an “elementary logos”

Egbert Rijke: Synthetic Homotopy Theory

  • deloop the 3-sphere: find a pointed connected type X s.th Omega(X) = S^3

  • define the Grassmanians (& other interesting CW-complexes) using HITS.

  • prove the BoTT periodicity theorem

Jonas Frey: The Coherence Problem

  • define internal operads, semi-simplicial types, (oo,1)-categories in HoTT.

Anders Mortberg: Cubical Type Theory

  • Efficient evaluation/ computation of cubical programs

  • have a cubical TT where transport ref x == x.

Guillaume Brunerie: Computation in Cubical Type Theory

  • find other interesting examples of cubical terms to compute (e.g. cohomology cup products)

Kristina Sojakova:

  • conservativity of cubical TT over Book HoTT

  • does adding a path between fixed points in a type preserve truncation level?

  • if X is an n-type for n > 0 and a, b : X, is the HIT H generated by [-] : X —> H , p : [a] = [b] , still an n-type? (Kristina: true?)

Steve Awodey:

  • crossed modules classify 2-types

  • define a notion of cubical quasi-category

  • Cubical Homotopy Hypothesis: sSet (w/Kan QMS) ~ cSet (Dedekind cubes w/Sattler QMS)

Return to open problems.

Revision on August 10, 2019 at 23:08:36 by steveawodey?. See the history of this page for a list of all contributions to it.