@Matthew – I think there's a typo in your (4):

> 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\\)

because what you've proved is

> 4: \\(\Phi(-, y) : \mathcal{X}^{\mathrm{op}} \rightarrow \mathcal{V}\\) and \\(\Phi(x, -) : \mathcal{Y} \rightarrow \mathcal{V}\\) are both \\(\mathcal{V}\\)-functors for all \\(x,y\\)

fwiw the Yoneda lemma has always puzzled me because it seems to rely on some trick involving "special" properties of **Set** (in particular the role **Set** plays in defining "plain vanilla" categories). I once asked a category theoretician friend of mine what this "special" was exactly, and he replied "symmetric monoidal closed". Anyway, I think I'm getting reasonably close to understanding his answer, albeit over a decade later.

> 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\\)

because what you've proved is

> 4: \\(\Phi(-, y) : \mathcal{X}^{\mathrm{op}} \rightarrow \mathcal{V}\\) and \\(\Phi(x, -) : \mathcal{Y} \rightarrow \mathcal{V}\\) are both \\(\mathcal{V}\\)-functors for all \\(x,y\\)

fwiw the Yoneda lemma has always puzzled me because it seems to rely on some trick involving "special" properties of **Set** (in particular the role **Set** plays in defining "plain vanilla" categories). I once asked a category theoretician friend of mine what this "special" was exactly, and he replied "symmetric monoidal closed". Anyway, I think I'm getting reasonably close to understanding his answer, albeit over a decade later.