re **Puzzle 280** I think @Reuben is right that we can solve this using the [Eckmann-Hilton argument](https://ncatlab.org/nlab/show/Eckmann-Hilton+argument) mentioned [earlier](https://forum.azimuthproject.org/discussion/comment/19025/#Comment_19025) in this course. Here's as far as I've got.
First note that Puzzle 278 is basically an "exchange law":
\[(f\otimes g)\circ(h\otimes k) = (f\circ h)\otimes(g\circ k)\]
In the special case where \\(f, k : I \to I\\) and \\(g = h = 1_I\\) we get
\[(f\otimes 1)\circ(1\otimes k) = (f\circ 1)\otimes(1\circ k) = f\otimes k\]
But we also have
\[f\otimes k = (1\circ f)\otimes(k\circ 1) = (1\otimes k)\circ(f\otimes 1)\]
This tells us
\[(f\otimes 1)\circ(1\otimes k) = (1\otimes k)\circ(f\otimes 1)\]
... which is *almost* \\(f\circ k = k\circ f\\) but not quite.
I think we need to mess about with with left/right unitors and coherence equations to iron out this final step.
First note that Puzzle 278 is basically an "exchange law":
\[(f\otimes g)\circ(h\otimes k) = (f\circ h)\otimes(g\circ k)\]
In the special case where \\(f, k : I \to I\\) and \\(g = h = 1_I\\) we get
\[(f\otimes 1)\circ(1\otimes k) = (f\circ 1)\otimes(1\circ k) = f\otimes k\]
But we also have
\[f\otimes k = (1\circ f)\otimes(k\circ 1) = (1\otimes k)\circ(f\otimes 1)\]
This tells us
\[(f\otimes 1)\circ(1\otimes k) = (1\otimes k)\circ(f\otimes 1)\]
... which is *almost* \\(f\circ k = k\circ f\\) but not quite.
I think we need to mess about with with left/right unitors and coherence equations to iron out this final step.
Version 2.1.8p2
