9
$\begingroup$

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.

Improve this question
$\endgroup$
3
  • 1
    $\begingroup$ Have you consulted this? arxiv.org/abs/0904.0125 $\endgroup$
    – Todd Trimble ♦
    Apr 3, 2016 at 20:40
  • $\begingroup$ I saw it. It looks interesting, but I have not looked into it yet. I wonder if it answers some of my questions. $\endgroup$
    – Dimitri Chikhladze
    Apr 3, 2016 at 23:11
  • 1
    $\begingroup$ 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. $\endgroup$
    – Paul Taylor
    Apr 6, 2016 at 15:12

1 Answer 1

Reset to default
3
$\begingroup$

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
Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .