Here are the open problems stated at the HoTT 2019 Summer School, listed by the instructor who posed the problem:
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”
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
Efficient evaluation/ computation of cubical programs
have a cubical TT where transport ref x == x.
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?)
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.