In addition to Tibor Béke, one should also mention the work of Jonathan Cohen. I’ll get to this at some point. (I hope.)

If I recall correctly, the Mac Lane-Paré paper is similar in its syntactic methodology to the usual Mac Lane proof. There is a more “semantic” proof of the coherence theorem based on the Yoneda embedding, described in various places (such as Braided Tensor Categories, without mentioning Yoneda however). In outline, for bicategories $B$, one embeds $B$ locally fully and faithfully in the *strict* 2-category $Cat^{B^{op}}$. Checking all the details requires a few diagram chases, but overall this is a very attractive alternative strategy.

I think it is OK to have a separate entry for so long specific proof, as Yaron has concluded.

By the way, another, more general approach, in terms of indexed categories, having the MacLane coherence theorem as a corollary is the subject of a paper

- S. MacLane, R. Paré,
*Coherence for bicategories and indexed categories*, J. Pure Appl. Algebra , 37 (1985) pp. 59–80

Another very general method using 2-rewriting systems is in a recent paper of Tibor Béke. Maybe we should incorporate and comment these references in one of the entries on coherences. This week will be again tough with me, with administrative deadlines, hosting scientific guest and a longer medical appointment, so likely not me.

]]>Thanks, Urs! I’ve put this in a separate entry to avoid cluttering Todd’s advanced comments.

]]>I forgot to say: awesome that you have produced this entry!

]]>I have added links back and forth with the stub coherence theorem for monoidal categories. Maybe the two entries should be merged into one?

]]>I’ve moved part of my beginner’s summery on Mac Lane’s proof of the coherence theorem for monoidal categories to the $n$Lab.

Surely there are many mistakes, possibly fatal: I am most worried about the naive definition I used for the syntax of arrows (sadly, I could only use my nearly zero knowledge of logic), and the part including the units and unitors. There are probably many itex errors too.

At some point I’ve realized that it was silly to use the cumbersome arrow language as is (say, writing a string like $\alpha u v u$ instead of $\alpha_{u,v,w}$, etc.), but to correct this required changing all figures, and this is too much for me at the moment. I also apologize for using files for figures (admiting that some of them shouldn’t even be figures), but it was too much work to do all the transition from my notes to itex in one jump.

I hope learning by seeing this page modified by people knowing more than me (anyone here, that is :) ), but if this page seems beyond hope, I have no objections to renaming it so that it will not clutter the ’lab.

By the way, now that I’ve re-entered the page, all figures appear with a question mark, and to the see the figure I have to press on the question-mark link (previously I’ve seen all figures appearing in the page). Is there any way to solve this problem?

]]>