Pentagon identity for a monoidal category (source code)

= Pentagon identity for a monoidal category

For an <associator> $a$ in a <monoidal category>, the two paths from $((W\otimes X)\otimes Y)\otimes Z$ to $W\otimes(X\otimes(Y\otimes Z))$ agree:
$$
a_{W,X,Y\otimes Z}a_{W\otimes X,Y,Z}=(1_W\otimes a_{X,Y,Z})a_{W,X\otimes Y,Z}(a_{W,X,Y}\otimes1_Z).
$$
This five-vertex diagram is the basic compatibility for reassociating four tensor factors. The <monoidal coherence theorem> extends it to arbitrary finite tensor expressions.