What is the status of (universal) algebra in type theory? 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?
 A: 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!
A: I'm not sure exactly what you have in mind, but I would suggest that you shouldn't take too narrow a view of what it means to "develop algebra within the framework of type theory".  For example, one of the major announcements last year was the completion of the formalization of the Feit-Thompson theorem in Coq.  Perhaps the theory of finite groups doesn't qualify as "universal algebra", though.  On the other hand, the so-called "problem of computational effects" in the semantics of programming languages has led to much cross-breeding between the two areas of type theory and universal algebra, and a pretty extensive literature; for some background, see Martin Hyland and John Power's The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads.
Nevertheless, I think it's fair to say that we still don't have a very good understanding of the connection between the important concepts of universal algebra and the important concepts of type theory---and that developing such a connection is a worthwhile task indeed.
