With the recent interest in homotopy type theory as a foundation for mathematics, it seems natural to develop algebra within the framework of type theory. So far, I can't find much literature regarding this.


I know of Danielsson and Coquand's result that isomorphism implies equality, and work by Spitters and van der Weegen using type classes (without univalence), but has any other work been done to develop algebra within dependent type theory? Is this even a worthwhile task?



What is the status of (universal) algebra in type theory?
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!


