# 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, 2016 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, 2016 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, 2016 at 15:12