> I think we can simplify that slightly @Matthew

>

> We have your (A) and (B), ie \\(x\otimes (x\multimap y) \leq y\\) and \\(y \otimes (y\multimap z) \leq z\\).

Sure, but it's important to note that we are using commutativity to flip (B).

> Therefore \\(x\otimes (x\multimap y) \otimes (y\multimap z) \leq y \otimes (y\multimap z) \leq z\\).

>

> So by adjunction \\((x\multimap y) \otimes (y\multimap z) \leq (x\multimap z)\\).

Again, you are using commutativity...

That's pedantry, I know. The proof is ugly and long if we don't just use commutativity implicitly.

However, I am not sure if this theorem is true in a closed non-commutative monoidal preorder.

>

> We have your (A) and (B), ie \\(x\otimes (x\multimap y) \leq y\\) and \\(y \otimes (y\multimap z) \leq z\\).

Sure, but it's important to note that we are using commutativity to flip (B).

> Therefore \\(x\otimes (x\multimap y) \otimes (y\multimap z) \leq y \otimes (y\multimap z) \leq z\\).

>

> So by adjunction \\((x\multimap y) \otimes (y\multimap z) \leq (x\multimap z)\\).

Again, you are using commutativity...

That's pedantry, I know. The proof is ugly and long if we don't just use commutativity implicitly.

However, I am not sure if this theorem is true in a closed non-commutative monoidal preorder.