nLab HoTT2019 Summer School open problems list

Here are the open problems stated at the HoTT 2019 Summer School (on homotopy type theory), listed by the instructor who posed the problem:

Mathieu Anel: Logos Theory

• Notion of higher theory? (syntactic approach? categorical approach à la Lawvere?) (e.g. CAT^lex, CAT_cc, LOGOS, …)

• Explicit distributivity formula between finite limits and colimit in a logos? colim_{something} lim_{something} —> lim_{something} colim_{something} This should lead to a polynomial calculus for logoi (in the sense of polynomial functors)

• Explicit description of the symmetric logo functor? Sym: CAT_cc —> LOGOI

• Develop internal cat theory in a logos

• Define a class of logoi suited for the purpose of logic (and containing all presentable logoi)

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

• (suggested by Nicolai Kraus): Does adding a path between fixed points in a type preserve truncation level? Namely, 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?

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 in homotopy type theory.