Ahh, I see what you mean. It isn't clear from the diagram that the \\(\le\\) nodes are _specific_ reactions (the reflexivity reactions), not just _any_ reactions. (Though, I'm not sure equality of diagrams is obvious enough to be used here, since that amounts to an equality of _proofs_, and it isn't clear that these proofs are equal at all.)

Actually, I would argue that what you've produced is a proof that \\((x \otimes y) \otimes z \le x \otimes (y \otimes z)\\). (Or \\(\ge\\), depending on the convention.) You can get the other direction by doing the analogous proof with \\(y \otimes z \le y \otimes z\\) at the bottom. Of course, you've implicitly used associativity to begin with to construct your proof.

If we didn't have associativity, we would need to explicitly bind arrows together, and reaction nodes \\(\le\\) could only relate one input wire to one output wire (where those wires were pre/post-bound separately from the relation). It's only because we don't care at all about how wires are grouped that we can "implicitly" dovetail wires at the reaction sites.

Actually, I would argue that what you've produced is a proof that \\((x \otimes y) \otimes z \le x \otimes (y \otimes z)\\). (Or \\(\ge\\), depending on the convention.) You can get the other direction by doing the analogous proof with \\(y \otimes z \le y \otimes z\\) at the bottom. Of course, you've implicitly used associativity to begin with to construct your proof.

If we didn't have associativity, we would need to explicitly bind arrows together, and reaction nodes \\(\le\\) could only relate one input wire to one output wire (where those wires were pre/post-bound separately from the relation). It's only because we don't care at all about how wires are grouped that we can "implicitly" dovetail wires at the reaction sites.