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

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

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:

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

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