# 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?

-
Probably the best existing construction at the moment is that of just oridnary category theory internal to HoTT, by Ahrens, Kapulkin and Shulman, see here: ncatlab.org/nlab/show/… . From there on one should develop $\infty$-category theory internal to HoTT, then $\infty$-operads/$\infty$-monads based on this, and thus universal algebra. It's sort of clear how to do this, but currently there is one stupid lttle stumbling block: simplicial objects currently don't work in fully formal (computer coded)HoTT –  Urs Schreiber Oct 14 '13 at 17:33
@Urs: the problem with simplicial objects isn’t just in “fully formal (computer-coded) HoTT”; it’s an issue in HoTT of any kind. And in my opinion (and I think most people’s who’ve tried to get past it) it’s more than a technical stumbling-block — it’s an interesting and non-trivial problem. All the classical approaches to homotopical algebraic structures seem to use on-the-nose equality in an essential way at some point — the simplicial identities, the axioms for an operad action, etc. To do algebra on non-truncated types in HoTT needs an approach that never goes via that at all. –  Peter LeFanu Lumsdaine Oct 17 '13 at 15:41
@Urs: the internal approach to the type theory of simplicial objects is not solving exactly the same problem as defining simplicial types would do. It may be usable to address some of the same issues, but probably not all of them. In the long run, I think we'll need to address the other question as well. –  Mike Shulman Oct 26 '13 at 22:40
BTW, I think anyone who's going to call them "Ahrens-Kapulkin-Shulman categories" should at least also add Voevodsky to the list of people. He had the same idea at about the same time, and inspired Benedikt and Chris to formalize it, even though he didn't help write the paper. (He called them "categories" and "saturated categories" instead of "precategories" and "categories".) –  Mike Shulman Oct 26 '13 at 22:44
@UrsSchreiber: The “‘ordinary formal’ mathematics of higher topos theory”? That’s HTT, not HoTT! They’re (somehow) connected, but not the same; in particular, when you do HTT, you have lots of ‘external’ methods available that you don’t have when working in HoTT. And I also wouldn’t necessarily claim that one ‘needs to add on-the-nose equality to do simplicial types’ [or semi-simplicial, etc.]; I’m just saying we haven’t worked out yet how to do them without it. –  Peter LeFanu Lumsdaine Oct 28 '13 at 22:41

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!

-
Re #1: Danielsson–Coquand consider cubical homotopy theory in 0-types, but that's not what is usually considered as universal algebra of 0-types. Re #2: what to expect is clear, namely "Higher algebra" as here ncatlab.org/nlab/show/Higher+Algebra . –  Urs Schreiber Oct 18 '13 at 8:20
I would expect the universal algebra of 1-types to look mostly like bicategorical monad theory. Classical 2-monad theory makes a lot of use of strict 2-categories and 2-functors; doing without that involves a lot more coherence. –  Mike Shulman Oct 26 '13 at 22:45
I guess I should go ahead and mark this question as answered. Many thanks to everyone, particularly Peter and Urs. –  Cory Knapp Oct 28 '13 at 18:14

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.

-