(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.
>
> $\overline{\textbf{Cost}}(x,y) =\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:

\begin{align} \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} \end{align}

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