Ah, now I get what you are saying. You are looking at this in comment #21:

> > **Lemma.** If \$$\mathcal{V}\$$ is monoidal partial order which also an [upper semilattice](https://en.wikipedia.org/wiki/Semilattice#Complete_semilattices) with arbitrary joins, then it is closed.
>
> **Proof.** Just define
>
> $x \multimap y := \bigvee\lbrace z\mid z\otimes x \leq y\rbrace$
>
> We know that this exists because \$$\mathcal{V}\$$ has arbitrary joins. We have \$$(A \otimes -) \dashv (A \multimap -)\$$ from an old result back in [Lecture 6](https://forum.azimuthproject.org/discussion/1901/lecture-6-chapter-1-computing-adjoints/). \$$\qquad \blacksquare \$$
>
> The above argument doesn't need \$$\otimes\$$ to distribute over \$$\bigvee\$$ as far as I can tell. I believe it is necessary to define profunctor composition, however.

I meant I didn't use the assumption that \$$\otimes\$$ distributes in the little lemma.

I didn't mean that I thought there was some closed monoidal partial order which didn't distribute. I hadn't thought about it. But I thought it was necessary to define composition, so I included it in my definition of *unital quantale* later inter comment #21.

For what it's worth, using John's separate definition of quantale I tried to show \$$\otimes\$$ distributes in [comment #1](https://forum.azimuthproject.org/discussion/comment/20224/#Comment_20224) of Lecture 63 assuming commutativity.