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?