[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.

If we go instead with

\[ 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.