Michael wrote:


Yes! This is an almost perfect pictorial explanation of the **interchange law**

\[ (f \circ f') \otimes (g \circ g') = (f \otimes g) \circ (f' \otimes g'). \]

As you note, it's a commutative square: tensoring and then composing equals composing and then tensoring.

A couple of nitpicky criticisms:

1) it's best to use arrows like this

\[ f \colon X \longrightarrow Y \]

or this

\[ X \stackrel{f}{\longrightarrow} Y \]

to stand for a function \\(f \\) from the set \\(X\\) to the set \\(Y\\) (or a morphism between objects), while using `\mapsto` arrows

\[ f \colon x \mapsto y \]

to indicate that the function \\(f\\) maps the element \\(x \in X\\) to the element \\(y \in Y\\). They are completely different kinds of arrows!

So I'd use \\(\mapsto\\) for the big arrows in your diagram.

2) A bit more importantly, two of your big arrows have complicated labels that do not describe those processes but rather the _result of applying_ those processes. I would probably write \\(\otimes\\) above the bottom horizontal arrow and \\( \circ \\) next to the right vertical arrow.