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.