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