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.