I think that we have the following definitions for the profunctors involved in the first snake equation:

\lambda_{\mathcal{X}}^{-1}(a, \langle 1, b \rangle) &= \mathcal{X}(a, b) \\\\
(\cap\_\mathcal{X} \otimes 1\_\mathcal{X})(\langle 1, b \rangle, \langle \langle c, c' \rangle, c'' \rangle) &= \mathcal{X}(c', c) \otimes \mathcal{X}(b, c'') \\\\
\alpha_{\mathcal{X}, \mathcal{X}^\mathrm{op}, \mathcal{X}}(\langle \langle c, c' \rangle, c'' \rangle, \langle d, \langle d', d'' \rangle \rangle) &= \mathcal{X}(c, d) \otimes \mathcal{X}(d', c') \otimes \mathcal{X}(c'', d'') \\\\
(1\_\mathcal{X} \otimes \cup\_\mathcal{X})(\langle d, \langle d', d'' \rangle \rangle, \langle e, 1 \rangle) &= \mathcal{X}(d, e) \otimes \mathcal{X}(d'', d') \\\\
\rho_\mathcal{X}(\langle e, 1 \rangle, f) &= \mathcal{X}(e, f). \\\\

Using the definition of composition and the fact that \\(\mathcal{V}\\) is a commutative quantale, we get the composition of the above profunctors to be

\bigvee_{b, c, c', c'', d, d', d'', e} \mathcal{X}(a, b) \otimes \mathcal{X}(c', c) \otimes \mathcal{X}(b, c'') \otimes \mathcal{X}(c, d) \otimes \mathcal{X}(d', c') \otimes \mathcal{X}(c'', d'') \otimes \mathcal{X}(d, e) \otimes \mathcal{X}(d'', d') \otimes \mathcal{X}(e, f).

This equation is equal to the idenity profunctor, \\(\mathcal{X}(a, f)\\), if

\bigvee_{y} \mathcal{X}(x, y) \otimes \mathcal{X}(y, z) = \mathcal{X}(x, z).

But I don't quite know how to show this – have we already proven this equation?

I think I know how to prove the last equation. We can use the two properties of the join:

- The join \\(j\\) is an upper bound; so for any \\(y\\) we have that \\(\mathcal{X}(x, y) \otimes \mathcal{X}(y, z) \le j\\). If we pick \\(y\\) to be \\(x\\) then we get that \\(\mathcal{X}(x,z) \le j\\).
- The join \\(j\\) is the _least_ upper bound; so for any other upper bound \\(u\\) we have that \\(j \le u\\). Since \\(\mathcal{X}(x,y) \otimes \mathcal{X}(y,z) \le \mathcal{X}(x, z)\\) for all \\(y\\), then \\(\mathcal{X}(x,z)\\) is an upper bound and \\(j \le \mathcal{X}(x, z)\\).

Hence, the join is exactly \\(\mathcal{X}(x,z)\\).