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.