Proving that a diagram involving associators and unitors commutes in a 2-category

149 Views Asked by At

In a 2-gategory, by coherence, the following equation holds for all $f : x \to y$ and $g : y \to z$: $$ \rho_{g * f} \; = \; \textit{id}_g * \rho_f \; \circ \; \alpha_{g, f, I_x} $$

Diagrammatically: sample image

How do you prove it starting from the usual triangle and pentagon coherence axioms?

Mumbling to myself: It is not a direct transformation of the triangle axiom because: it involves $\rho$ on both paths; and the $I_x$ is not the middle argument of $\alpha$, but is the last one. My guess is that the proof involves: the triangle and pentagon axioms, as well as the naturality of $\alpha$.

By the way, does this commutative diagram have a name?

1

There are 1 best solutions below

1
On BEST ANSWER

The analogous diagrams in the case of monoidal categories are proved to commute on the nlab here, as part of an explanation of how MacLane's original axioms for monoidal categories, which included your diagram, were cut down to just the pentagon and triangle axioms.

The same proofs work in a bicategory. We need that composing with an identity morphism is naturally isomorphic to the identity functor and therefore is an equivalence, that all of the coherence cells are invertible and natural, and the pentagon and triangle identities. All of these hold in bicategories just as they do in monoidal categories.

(As for the name of your diagram: I'd first check what MacLane named the corresponding axiom for monoidal categories. I'd be tempted to call it something like the 'right triangle identity', with a corresponding 'left triangle identity' for $I_z \circ (g \circ f)$ but I don't think that's standard terminology.)