I thought it might be worth explicitly spelling out the "profunctor rule" @Matthew mentions in his proof.

> **Theorem**: the following are equivalent:

> (1) \\(\qquad\Phi : \mathcal{X} \nrightarrow \mathcal{Y}\\) is a profunctor

> (2) \\(\qquad\mathcal{X}(a, x) \otimes \Phi(x, y) \otimes \mathcal{Y}(y, b) \leq \Phi(a, b)\\) for all \\(a, x, y, b\\)

>(3) \\(\qquad\mathcal{X}(a, x) \otimes \Phi(x, y) \leq \Phi(a, y)\\) and \\(\Phi(x, y) \otimes \mathcal{Y}(y, b) \leq \Phi(x, b)\\) for all \\(a, x, y, b\\)

**Proof**: (1) is true iff \\(\Phi : \mathcal{X}^\text{op} \times \mathcal{Y} \to \mathcal{V}\\) is a \\(\mathcal{V}\\)-functor, which is true iff

\[ (\mathcal{X}^\text{op} \times \mathcal{Y})((x, y), (a, b)) \leq \mathcal{V}(\Phi(x, y), \Phi(a, b)) \]

for all \\((x, y)\\) and \\((a, b)\\). Unwrapping the left and right hand sides, this is equivalent to

\[ \mathcal{X}(a, x) \otimes \mathcal{Y}(y, b) \leq \Phi(x, y) \multimap \Phi(a, b) \]

for all \\(a, x, y, b\\). But the adjunction definition of \\(\multimap\\) tells us that this is equivalent to

\[ \Phi(x, y) \otimes \mathcal{X}(a, x) \otimes \mathcal{Y}(y, b) \leq \Phi(a, b) \]

We can reorder the left hand side because \\(\otimes\\) is commutative – this shows that (1) is equivalent to (2).

Note that \\(I \leq \mathcal{X}(x, x)\\) and \\(I \leq \mathcal{Y}(y, y)\\) by the definition of a \\(\mathcal{V}\\)-category. So given (2) we can set \\(b = y\\) to get

\[ \mathcal{X}(a, x) \otimes \Phi(x, y) = \mathcal{X}(a, x) \otimes \Phi(x, y) \otimes I \leq \mathcal{X}(a, x) \otimes \Phi(x, y) \otimes \mathcal{Y}(y, y) \leq \Phi(a, y) \]

Or we can set \\(a = x\\) to get

\[ \Phi(x, y) \otimes \mathcal{Y}(y, b) = I \otimes \Phi(x, y) \otimes \mathcal{Y}(y, b) \leq \mathcal{X}(x, x) \otimes \Phi(x, y) \otimes \mathcal{Y}(y, b) \leq \Phi(x, b) \]

So (2) implies (3). Finally, assume (3) and then

\[ \mathcal{X}(a, x) \otimes \Phi(x, y) \otimes \mathcal{Y}(y, b) \leq \Phi(a, y) \otimes \mathcal{Y}(y, b) \leq \Phi(a, b) \]

so (3) implies (2) and we are done. QED