@Michael – I think you've got into a bit of a muddle there by confusing composition of \\(\mathcal{V}\\)-functors with composition of \\(\mathcal{V}\\)-profunctors.

For the latter we want to define a \\(\Psi\Phi : \mathcal{X} \nrightarrow \mathcal{Z}\\) for every pair \\(\Phi : \mathcal{X} \nrightarrow \mathcal{Y}\\) and \\(\Psi : \mathcal{Y} \nrightarrow \mathcal{Z}\\).

This amounts to defining a \\(\mathcal{V}\\)-functor \\(\Psi\Phi : \mathcal{X}^\text{op} \times \mathcal{Z} \to \mathcal{V}\\) for every pair of \\(\mathcal{V}\\)-functors \\(\Phi : \mathcal{X}^\text{op} \times \mathcal{Y} \to \mathcal{V}\\) and \\(\Psi : \mathcal{Y}^\text{op} \times \mathcal{Z} \to \mathcal{V}\\).

So our "composite profunctor" is *not* a composite of \\(\mathcal{V}\\)-functors.

Instead we *define* it by writing down its value in \\(\mathcal{V}\\) for any pair of objects \\(x \in \text{Ob}(\mathcal{X}^\text{op})\\) and \\(z \in \text{Ob}(\mathcal{Z})\\).

That's what this formula does:

\[ (\Psi\Phi)(x, z) = \bigvee\big(\Phi(x, y)\otimes\Psi(y, z)\big) \]

Then we need to check that this definition is a \\(\mathcal{V}\\)-functor, which means proving

\[ (\mathcal{X}^\text{op}\times \mathcal{Z})((x, z), (x', z')) \leq \mathcal{V}(\Psi\Phi)(x, z), (\Psi\Phi)(x', z')) \]

which in turn amounts to proving that

\[ \mathcal{X}(x', x) \otimes \mathcal{Z}(z, z') \leq (\Psi\Phi)(x, z)\multimap(\Psi\Phi)(x', z') \]

which in turn amounts to proving that

\[ \mathcal{X}(x', x) \otimes \bigvee\big(\Phi(x, y)\otimes\Psi(y, z)\big) \otimes\mathcal{Z}(z, z') \leq \bigvee\big(\Phi(x', y)\otimes\Psi(y, z')\big) \]

This is what we need to prove, and the trick here is to use the fact that \\(\otimes\\) preserves joins.

For the latter we want to define a \\(\Psi\Phi : \mathcal{X} \nrightarrow \mathcal{Z}\\) for every pair \\(\Phi : \mathcal{X} \nrightarrow \mathcal{Y}\\) and \\(\Psi : \mathcal{Y} \nrightarrow \mathcal{Z}\\).

This amounts to defining a \\(\mathcal{V}\\)-functor \\(\Psi\Phi : \mathcal{X}^\text{op} \times \mathcal{Z} \to \mathcal{V}\\) for every pair of \\(\mathcal{V}\\)-functors \\(\Phi : \mathcal{X}^\text{op} \times \mathcal{Y} \to \mathcal{V}\\) and \\(\Psi : \mathcal{Y}^\text{op} \times \mathcal{Z} \to \mathcal{V}\\).

So our "composite profunctor" is *not* a composite of \\(\mathcal{V}\\)-functors.

Instead we *define* it by writing down its value in \\(\mathcal{V}\\) for any pair of objects \\(x \in \text{Ob}(\mathcal{X}^\text{op})\\) and \\(z \in \text{Ob}(\mathcal{Z})\\).

That's what this formula does:

\[ (\Psi\Phi)(x, z) = \bigvee\big(\Phi(x, y)\otimes\Psi(y, z)\big) \]

Then we need to check that this definition is a \\(\mathcal{V}\\)-functor, which means proving

\[ (\mathcal{X}^\text{op}\times \mathcal{Z})((x, z), (x', z')) \leq \mathcal{V}(\Psi\Phi)(x, z), (\Psi\Phi)(x', z')) \]

which in turn amounts to proving that

\[ \mathcal{X}(x', x) \otimes \mathcal{Z}(z, z') \leq (\Psi\Phi)(x, z)\multimap(\Psi\Phi)(x', z') \]

which in turn amounts to proving that

\[ \mathcal{X}(x', x) \otimes \bigvee\big(\Phi(x, y)\otimes\Psi(y, z)\big) \otimes\mathcal{Z}(z, z') \leq \bigvee\big(\Phi(x', y)\otimes\Psi(y, z')\big) \]

This is what we need to prove, and the trick here is to use the fact that \\(\otimes\\) preserves joins.