Anindya wrote:

> One detail that puzzles me about the adjunction: the maps \\((x\otimes -)\\) and \\((x\multimap -)\\) are monotone but they don't seem to (necessarily) be *monoidal* monotone. So this is an adjunction between preorders, not an adjunction between monoidal preorders. That seems a bit unexpected to me.

It's actually familiar. One fundamental example of a monoidal preorder is a _group_, with \\(x \le y\\) iff \\(x = y\\), with \\( x \otimes y\\) defined to be the product \\(xy\\). This is closed if we define \\(x \multimap y = yx^{-1} \\), since the definition of 'closed'

\[ a \otimes x \le y \text{ if and only if } a \le x \multimap y \]

turns into

\[ ax = y \text{ if and only if } a = yx^{-1} \]

The moral is:

> **The monoidal structure is to multiplication as the closed structure is to division.**

But back to your point: multiplying by \\(x\\) is not a group homomorphism, nor is dividing by \\(x\\):

\[ (aa')x \ne (ax)(a'x) \]

and

\[ (yy')x^{-1} \ne (yx^{-1}) (y' {x}^{-1}) .\]

So, in the general case, we shouldn't want the maps \\((x\otimes -)\\) and \\((x\multimap -)\\) to be monoidal.

> One detail that puzzles me about the adjunction: the maps \\((x\otimes -)\\) and \\((x\multimap -)\\) are monotone but they don't seem to (necessarily) be *monoidal* monotone. So this is an adjunction between preorders, not an adjunction between monoidal preorders. That seems a bit unexpected to me.

It's actually familiar. One fundamental example of a monoidal preorder is a _group_, with \\(x \le y\\) iff \\(x = y\\), with \\( x \otimes y\\) defined to be the product \\(xy\\). This is closed if we define \\(x \multimap y = yx^{-1} \\), since the definition of 'closed'

\[ a \otimes x \le y \text{ if and only if } a \le x \multimap y \]

turns into

\[ ax = y \text{ if and only if } a = yx^{-1} \]

The moral is:

> **The monoidal structure is to multiplication as the closed structure is to division.**

But back to your point: multiplying by \\(x\\) is not a group homomorphism, nor is dividing by \\(x\\):

\[ (aa')x \ne (ax)(a'x) \]

and

\[ (yy')x^{-1} \ne (yx^{-1}) (y' {x}^{-1}) .\]

So, in the general case, we shouldn't want the maps \\((x\otimes -)\\) and \\((x\multimap -)\\) to be monoidal.