Hey John,

I was thinking about Anindya's theorem from [comment #12](https://forum.azimuthproject.org/discussion/comment/20252/#Comment_20252) of Lecture 63, which you reposted here.

I wanted to extend it:

> **Theorem.** In a commutative quantale \$$\mathcal{V}\$$, the following are equivalent:
>
> 1. \$$\Phi : \mathcal{X} \nrightarrow \mathcal{Y}\$$ is a \$$\mathcal{V}\$$-enriched profunctor.
>
> 2. \$$\mathcal{X}(x', x) \otimes \Phi(x, y) \otimes \mathcal{Y}(y, y') \leq \Phi(x',y')\$$ for all \$$x,x',y,y'\$$.
>
> 3. \$$\mathcal{X}(x', x) \otimes \Phi(x, y) \leq \Phi(x', y)\$$ and \$$\Phi(x, y) \otimes \mathcal{Y}(y, y') \leq \Phi(x, y')\$$ for all \$$x,x',y,y'\$$.
>
> 4. \$$\Phi(-, y) : \mathcal{X}^{\mathrm{op}} \Rightarrow \mathcal{V}\$$ and \$$\Phi(x, -) : \mathcal{Y} \Rightarrow \mathcal{V}\$$ are both \$$\mathcal{V}\$$-profunctors for all \$$x,y\$$

**Proof.**

Anindya already did most of the work back in [his comment to Lecture 63](https://forum.azimuthproject.org/discussion/comment/20252/#Comment_20252).

It suffices to show that (3) is equivalent to (4). Since \$$\mathcal{V}\$$ is a closed, commutative monoidal preorder, we have

$\mathcal{X}(x', x) \otimes \Phi(x, y) \leq \Phi(x', y) \iff \mathcal{X}^{\mathrm{op}}(x, x') \leq \Phi(x, y) \multimap \Phi(x', y) \tag(A)$

and

$\Phi(x, y) \otimes \mathcal{Y}(y, y') \leq \Phi(x, y') \iff \mathcal{Y}(y, y') \leq \Phi(x, y) \multimap \Phi(x, y'). \tag{B}$

But we also have

$\Phi(x, y) \multimap \Phi(x', y) = \mathcal{V}(\Phi(-,y)(x), \Phi(-,y)(x')) \tag{C}$

and similarly

$\Phi(x, y) \multimap \Phi(x, y') = \mathcal{V}(\Phi(x,-)(y), \Phi(x,-)(y')) \tag{D}$

with (A) and (C) along with (B) and (D) we have (3) is equivalent to (4). \$$\qquad \blacksquare \$$

If we take a \$$\mathcal{V}\$$-category \$$\mathcal{X}\$$, we know \$$\mathbf{hom}\_{\mathcal{X}}\$$ is the identity profunctor \$$1\_{\mathcal{X}}\$$. If \$$\mathcal{V} = \mathbf{Set}\$$, then \$$\mathbf{hom}\_{\mathcal{X}}(-, y)\$$ and \$$\mathbf{hom}\_{\mathcal{X}}(x, -)\$$ are the contravariant and covariant [Yoneda functors](https://en.wikipedia.org/wiki/Yoneda_lemma#The_Yoneda_embedding), respectively.

The Yoneda Lemma, which holds for \$$\mathbf{Set}\$$-enriched categories, states for any functor \$$F\$$:

$\mathrm{Nat}(\mathbf{hom}\_{\mathcal{X}}(A, -), F) \cong F(A)$

It may be beyond the purview of this course, but I am rather curious what sort of enriched categories \$$\mathcal{V}\$$ the Yoneda lemma generalizes to...