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...