# Homotopy Type Theory HoTT2019 Summer School open problems list (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

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 Notion of higher theory? (CAT^lex, (syntactic approach? categorical approach à la Lawvere?) (e.g. CAT^lex, CAT_cc, LOGOS, …)

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

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

• Develop internal cat theory in a logos

• define Define an a “elementary class logos” 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

• 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)