[Anindya](https://forum.azimuthproject.org/discussion/comment/20082/#Comment_20082) wrote:

> One detail that puzzles me about the adjunction: the maps \$$(x\otimes -)\$$ and \$$(x\multimap -)\$$ are monotone but ...

You know, there might be a typo in the lecture notes.

I usually see \$$(x\otimes -) \dashv (x\multimap -)\$$. For instance, this is how the Haskell adjunctions library defines them (see [the hackage docs](https://hackage.haskell.org/package/adjunctions-4.0.2/docs/Data-Functor-Adjunction.html#t:Adjunction)).

But in the lecture notes, John wrote

> $a \otimes x \le y \text{ if and only if } a \le x \multimap y \tag{✴}$

So technically \$$(- \otimes x) \dashv (x\multimap -)\$$ if we don't assume commutativity.

$x \otimes a \le y \text{ if and only if } a \le x \multimap y \tag{✴'}$
Then your quick proof in [#6](https://forum.azimuthproject.org/discussion/comment/20080/#Comment_20080) works, the theorem we proved holds without demanding commutativity, and \$$(x\otimes -) \dashv (x\multimap -)\$$ like you say.