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.

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