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
> **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
Version 2.1.8p2
