It largely depends on how general you want to make your algebra; in particular, do you want to look just at structures on $n$-types, for some finite $n$, or consider algebraic structures on all types?

**The universal algebra of 0-types should look much like classical universal algebra;** this is what the Danielsson–Coquand result you mention talks about, for instance, and as far as I know no general work beyond that has been done yet. The most novel aspects of this, I guess, would be in giving more exploration of working with Ahrens–Kapulkin–Shulman categories (and related structures) than anyone’s done so far.

**The universal algebra of 1-types is wide open, and should be reasonably approachable.** I don’t know of any existing work in this direction; and I also don’t know quite what to expect it to look like — possibly like classical 2-categorical algebra (in the 2-monad sense), or possibly nicer, if AKS–style (2-)categories give a simplification of the language? Algebra on $n$-types, for fixed $n>1$, is also open, but I guess this would be a subsequent project to the 1-types case.

**Algebra on arbitrary types is open, but probably difficult.** Several of us at the IAS last year spent some time trying to crack this (not for general u.a., just for specific algebraic structures), and all ran up against the barrier that Urs alludes to in comments. Essentially, classical approaches to coherently homotopy-algebraic structures seem to all sooner or later use on-the-nose equality in some way that’s not available in HoTT (e.g. the axioms of an operad action). This is a known open problem, and a nice one, but not easy, I think!

8more comments