Recall Mac Lane's version of coherence for monoidal categories, which one can state informally as follows:

"Simple-minded" coherence for monoidal categoriesLet $A$, $A^\prime$ be two bracketings on the monoidal product $A_{1} \otimes \ldots \otimes A_{n}$ (with possibly some additional occurances of the monoidal unit $I$). Let $i_{1}, i_{2}: A \rightarrow A^\prime$ be two isomorphisms built from associator and left/right unitors. Then $i_{1} = i_{2}$.

This theorem tells us that there is always canonical way to identify two products of $A_{1},\ldots, A_{n}$ with possibly different bracketings. Here I say "simple-minded" to mean that it can be presented as a statement of the form "some diagram commutes".

However, *coherence for monoidal categories* can also refer to the following result:

"Strictifying" coherence for monoidal categoriesAny monoidal category is equivalent to a strict monoidal category.

The strictifying version of coherence is an important theorem on its own right, but it also implies the simple-minded version of coherence with the following argument.

Let $i_{1}, i_{2}: A \rightarrow A^\prime$ be two isomorphisms as above in a monoidal category $M$ and let $T: M \rightarrow N$ be an equivalence into a strict monoidal category. Then $T(i_{1}), T(i_{2})$ are both isomorphic to analogous composites of associators and left/right unitors in $N$, with the isomorphism given by constraint cells of $T$. Since $N$ is strict, the analogous composites in $N$ are both equal to the identity and we conclude that $T(i_{1}) = T(i_{2})$.

(The argument seems to be well known, although I learned it from these short notes of Tom Leinster.)

My question concerns known results about such "simple-minded" coherence for monoidal bicategories (ie. one object tricategories), which I had trouble finding in the literature.

Recall that *coherence for tricategories* as proved by Gordon, Street, Power has the following form:

"Strictifying" coherence for tricategoriesAny tricategory is triequivalent to a

Gray-category, ie. to a category enriched over the category of strict 2-categories equipped with theGraytensor product. In particular, any monoidal bicategory is equivalent to aGraymonoid.

This is certainly an important and powerful result. However, what is not clear to me is how to extract from this some "simple-minded" corollaries, ie. statements about some diagrams (say, of 3-cells) commuting in any tricategory. I believe some argument similar in spirit to the one from notes of Tom Leinster should work, but triequivalences (or more generally, homomorphisms of tricategories) are such complicated objects that it is not quite obvious for me how to do this.

Is there any general framework for proving that some classes of diagrams commute in every tricategory? Has this been covered in the literature? What are the possible references?

For example, is the following naive generalization of Mac Lane coherence true?

"Naive" version of coherence for monoidal bicategoriesLet $A$, $A^\prime$ be two bracketings on the monoidal product $A_{1} \otimes \ldots \otimes A_{n}$ (with possibly some additional occurances of the monoidal unit $I$) in a monoidal bicategory. Let $i_{1}, i_{2}: A \rightarrow A^\prime$ be two 1-cells built from associators, left/right unitors and their pseudoinverses. Moreover, let $j_{1}, j_{2}: i_{1} \sim i_{2}$ be two isomorphisms built from the constraint $2$-cells. Then $j_{1} = j_{2}$.

Here I am using the algebraic definition of a monoidal bicategory, ie. the associatiors and unitors of the monoidal structure come with a chosen pseudoinverse and unit/counit modifications that make them into adjoint equivalences. I believe in this these unit/counit 2-cells should also be considered "constraint", but I hope I can be forgiven for leaving this a little vague just to see what might be true and what isn't.

I stumbled upon this type of questions while studying possible definitions of a *dual pair* of objects in a monoidal bicategory. I frequently find it very problematic to prove any uniqueness results due to the relevant computations being difficult. Hence, I am looking for techniques that could simplify working with a general tricategory.