(Edit: I have changed my notation regarding unital quantales based on Anindya's comments below)

Returning to my puzzle:

> How do we define \\(\mathcal{V}\\)-profunctor composition?

I was going back to something Simon Willerton said in [Lecture 59](https://forum.azimuthproject.org/discussion/comment/20044/#Comment_20044) when he was showing how \\(\mathbf{Cost}\\) can be turned into a \\(\mathbf{Cost}\\)-functor:

> You take
> \[
\overline{\mathcal{V}}(x,y)=\bigvee\lbrace z\mid z\otimes x \rtimes y\rbrace.
> This will work provided that the poset has the requisite joins, and that \\(\otimes\\) distributes over joins. And because it is a *poset* rather than a preorder, the join will be unique.
> In the case of \\(\textbf{Cost}\\) you get the following.
> \[
=\inf\\{z\mid z + x \ge y\\}
=\max(y-x, 0).

Based on Simon's comment, we have the following:

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

(EDIT: As noted in [comment #67](https://forum.azimuthproject.org/discussion/comment/20251/#Comment_20251), this is incorrect)

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

To this end, I suggest a new definition:

> **Definition.** A structure \\(\mathcal{V} = (X, \leq, \bigvee, \bot, \otimes, I)\\) is called a [unital quantale](https://en.wikipedia.org/wiki/Quantale) when
> 1. \\((X, \leq, \otimes, I)\\) is a monoidal poset
> 2. \\((X,\leq,\bigvee, \bot)\\) is an [upper semilattice](https://en.wikipedia.org/wiki/Semilattice#Complete_semilattices) with arbitrary joins
> 3. \\((X,\bigvee, \otimes, I)\\) is a [complete-rig](https://en.wikipedia.org/wiki/Semiring#Complete_and_continuous_semirings), that is
> \[ \bigvee_{i \in I}{(a \otimes a_i)} = a \otimes \left(\bigvee_{i \in I}{a_i}\right); \quad \bigvee_{i \in I}{(a_i \otimes a)} = \left(\bigvee_{i \in I}{a_i}\right) \otimes a \]

So the lemma says that every unital quantale is a closed monoidal poset.

Back in [Lecture 58](https://forum.azimuthproject.org/discussion/2283/lecture-58-chapter-4-composing-feasibility-relations#latest), **Puzzle 181**, John Baez gave a definition of profunctor composition:

\[ (\Psi\Phi)(x,z) = \bigvee_{y \in \mathrm{obj}(\mathcal{Y})} \Phi(x,y) \otimes \Psi(y,z)\]

Now we need to show associativity. Here is where we use the distributive property Simon mentioned:

> **Lemma.** Let \\(\mathcal{V}\\) be a unital quantale, and let \\(\Phi : \mathcal{A} \nrightarrow \mathcal{B} \\), \\(\Psi : \mathcal{B} \nrightarrow \mathcal{C}\\), and \\(\Upsilon : \mathcal{C} \nrightarrow \mathcal{D}\\) be \\(\mathcal{V}\\)-profunctors. Then
> \[ (\Phi \Psi) \Upsilon = \Phi (\Psi \Upsilon) \]

**Proof.** To show this lemma need we need to establish a formula like the one I mentioned back in [Lecture 58](https://forum.azimuthproject.org/discussion/comment/20023/#Comment_20023):

\[ \bigvee_{c \in \mathrm{obj}(\mathcal{C})} \left(\bigvee_{b \in \mathrm{obj}(\mathcal{B})} \Phi(a,b) \otimes \Psi(b,c)\right) \otimes \Upsilon(c,d) =
\bigvee_{b \in \mathrm{obj}(\mathcal{B})} \Phi(a,b) \otimes \left(\bigvee_{c \in \mathrm{obj}(\mathcal{C})} \Psi(b,c) \otimes \Upsilon(c,d) \right) \]

Let's walk through how to get to this:

\bigvee_{c \in \mathrm{obj}(\mathcal{C})} \left(\bigvee_{b \in \mathrm{obj}(\mathcal{B})} \Phi(a,b) \otimes \Psi(b,c)\right) \otimes \Upsilon(c,d)
& = \bigvee_{c \in \mathrm{obj}(\mathcal{C})} \left(\bigvee_{b \in \mathrm{obj}(\mathcal{B})} \Phi(a,b) \otimes \Psi(b,c) \otimes \Upsilon(c,d) \right) \tag{by distributivity} \\\\
& = \bigvee_{b \in \mathrm{obj}(\mathcal{B})} \left(\bigvee_{c \in \mathrm{obj}(\mathcal{C})} \Phi(a,b) \otimes \Psi(b,c) \otimes \Upsilon(c,d) \right) \tag{upper semi-lattice identity} \\\\
& = \bigvee_{b \in \mathrm{obj}(\mathcal{B})} \Phi(a,b) \otimes \left(\bigvee_{c \in \mathrm{obj}(\mathcal{C})} \Psi(b,c) \otimes \Upsilon(c,d) \right) \tag{by distributivity}

The only novel trick is that upper semi-lattice identity I mentioned, which I'll go over later if anyone is confused. \\( \qquad \blacksquare \\)

So we almost have a category of \\(\mathcal{V}\\)-profunctors, all we need now are suitable \\(\mathcal{V}\\)-profunctors to be our identity morphisms...