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.