> **Puzzle 199.** Suppose that \$$\mathcal{V}\$$ is a commutative quantale. Show that composition of \$$\mathcal{V}\$$-enriched profunctors is associative.

I tried to prove this in [comment #21](https://forum.azimuthproject.org/discussion/comment/20204/#Comment_20204) of lecture 62, but I used Wikipedia's definition of a unital quantale.

My old attempted proof uses the following distributive laws:

$a \otimes \left( \bigvee\_{b\in B} b\right) = \bigvee\_{b \in B} (a \otimes b) \quad ; \quad \bigvee\_{b\in B} (b \otimes a) = \left(\bigvee\_{b \in B} b\right) \otimes a$

Since we are assuming \$$\mathcal{V}\$$ is commutative, we only need to prove one of these.

Recalling the definition of a quantale, we have:

> **Definition.** A **quantale** is a closed monoidal poset \$$\mathcal{V}\$$ that has all joins: that is, every subset of \$$S\subseteq \mathcal{V}\$$ has a least upper bound \$$\bigvee S\$$.

Hence we know that \$$\mathcal{V}\$$ has an adjoint \$$(A \otimes -) \dashv (A \multimap -)\$$ from [Lecture 61](https://forum.azimuthproject.org/discussion/2291/lecture-61-chapter-4-closed-monoidal-posets/p1).

Next, we want to show \$$a \otimes \bigvee_{b \in B} b \leq c \iff \bigvee_{b \in B} (a \otimes b) \leq c\$$. Using the adjunction from Lecture 61 we have the following chain of biconditionals:

\begin{align} a \otimes \left(\bigvee_{b \in B} b\right) \leq c & \iff \bigvee_{b \in B} b \leq a \multimap c \\\\ & \iff \text{for all } b \text{ in } B \text{: } b \leq a \multimap c \\\\ & \iff \text{for all } b \text{ in } B \text{: } a \otimes b \leq c \\\\ & \iff \bigvee_{b \in B} (a \otimes b) \leq c \\\\ \end{align}

We know that \$$a \otimes \left(\bigvee_{b \in B} b\right) \leq a \otimes \left(\bigvee_{b \in B} b\right)\$$ by reflexivity, hence \$$\bigvee_{b \in B} (a \otimes b) \leq a \otimes \left(\bigvee_{b \in B} b\right)\$$. Similarly, we know \$$\bigvee_{b \in B} (a \otimes b) \leq \bigvee_{b \in B} (a \otimes b) \$$, hence \$$a \otimes \left(\bigvee_{b \in B} b\right) \leq \bigvee_{b \in B} (a \otimes b) \$$. Thus \$$a \otimes \left(\bigvee_{b \in B} b\right) = \bigvee_{b \in B} (a \otimes b) \$$.

Now that distributivity is established, my old proof should apply. I will reiterate it.

Let \$$\Phi : \mathcal{A} \nrightarrow \mathcal{B} \$$, \$$\Psi : \mathcal{B} \nrightarrow \mathcal{C}\$$, and \$$\Upsilon : \mathcal{C} \nrightarrow \mathcal{D}\$$ be \$$\mathcal{V}\$$-profunctors. We need to show

$(\Phi \Psi) \Upsilon = \Phi (\Psi \Upsilon)$

Expanding the definition of profunctor composition, this amounts to showing:

$\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{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}

\$$\qquad \blacksquare \$$

As a note, Anindya remarks in [comment #22](https://forum.azimuthproject.org/discussion/comment/20205/#Comment_20205) of Lecture 62 there may be issues with that lattice identity I have tried to use...