# Coherence and rewriting

In category theory there are numerous coherence theorems (https://ncatlab.org/nlab/show/coherence+theorem). One example is the Mac Lane's coherence theorem for monoidal categories. This and probably others as well, I believe, can be formulated in the language of term rewriting (https://en.wikipedia.org/wiki/Rewriting).

What work has been done in the term rewriting theory related to coherence in category theory? Are there general results in the term rewriting theory from which various categorical coherence theorems follow?

There may be some advantages to the term rewriting formulation in practice too. For example, analogous to a monoidal category, one can define a pseudomonoid (also called a monoidale) internal to a monoidal 2-category. This should satisfy coherence similar to Mac Lanes's coherence, which will involve 2-cells rather than natural transformations. Some other similar coherences also can occur (see Pseudomodules, "general coherence theorem"). I think that all these should follow from one term rewriting result.

I am also interested in term rewriting for higher categorical coherence.

• Have you consulted this? arxiv.org/abs/0904.0125 Apr 3 '16 at 20:40
• I saw it. It looks interesting, but I have not looked into it yet. I wonder if it answers some of my questions. Apr 3 '16 at 23:11
• There were applications of category theory to term rewriting in the mid 1990s. The appropriate structure turned out to be, not a 2-category, but a sesquicategory (sesqui- means $1\frac 1 2$) because the interchange law is inappropriate. I suggest a web search for this word. Apr 6 '16 at 15:12

There are two kinds of "coherence theorem". One of them states for example "bicategories are equivalent to 2-categories", the other kind are results that look like "every diagram of a certain form commute".

As far as I know, rewriting has only ever be applied to the second kind of problem. The basic result for proving this kind of thing is Squier's homotopical Theorem, and its extension by Guiraud and Malbos: http://arxiv.org/abs/0810.1442

• Guiraud and Malbos then used their theorem to prove coherence for monoidal, symmetric monoidal and braided monoidal categories: http://arxiv.org/abs/1004.1055
• I just recently uploaded this paper to the arXiv. Using the same technique as Guiraud and Malbos I am able to prove coherence for bicategories and pseudofunctors. I also prove coherence for pseudonatural transformations, but this requires significantly more work http://arxiv.org/abs/1508.07807