Here are the open problems stated at the [HoTT 2019 Summer School](https://hott.github.io/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]].