Hey Anindya,

I'll give this a shot. I'll just do the analogue **Puzzle 173** for now...

> Suppose \\(\mathcal{V}\\) is a closed commutative monoidal poset and \\(\mathcal{X}\\) and \\(\mathcal{Y}\\) are \\(\mathcal{V}\\)-categories.
> **Puzzle AB 173.** Assume \\(F : \mathcal{X} \to \mathcal{Y} \\) is a \\(\mathcal{V}\\)-functor from \\(\mathcal{X}\\) to \\(\mathcal{Y}\\). Prove that there is a \\(\mathcal{V}\\)-profunctor \\(\Phi : \mathcal{X} \nrightarrow \mathcal{Y}\\) given by \\(\Phi(x,y) = \mathcal{Y}(F(x), y)\\).

To start, to show \\(\Phi\\) is a \\(\mathcal{V}\\)-profunctor we need to show it is a \\(\mathcal{V}\\)-functor \\( \Phi : \mathcal{X}^{\text{op}} \times \mathcal{Y} \to \mathcal{V} \\)

Following the logic we worked out in #6, we need to show

\[ (\mathcal{X}^{\mathrm{op}} \times \mathcal{Y})((a,b),(c,d)) \leq \Phi(a,b) \multimap \Phi(c,d) \]

Once again, we'll use the identity

\[ (\mathcal{X}^{\text{op}} \times \mathcal{Y})((a,b),(c,d)) = \mathcal{X}(c,a) \otimes \mathcal{Y}(b,d) \]


(\mathcal{X}^{\mathrm{op}} \times \mathcal{Y})((a,b),(c,d)) \leq \Phi(a,b) \multimap \Phi(c,d) & \iff \mathcal{X}(c,a) \otimes \mathcal{Y}(b,d) \leq \Phi(a,b) \multimap \Phi(c,d) \\\\
& \iff \mathcal{X}(c,a) \otimes \mathcal{Y}(b,d) \leq \mathcal{Y}(F(a), b) \multimap \mathcal{Y}(F(c), d) \\\\
& \iff \mathcal{Y}(F(a), b) \otimes \mathcal{X}(c,a) \otimes \mathcal{Y}(b,d) \leq \mathcal{Y}(F(c), d)\ .

So it suffices to show
\[ \mathcal{Y}(F(a), b) \otimes \mathcal{X}(c,a) \otimes \mathcal{Y}(b,d) \leq \mathcal{Y}(F(c), d) \]

Because \\(F\\) is a \\(\mathcal{V}\\)-functor we know \\(\mathcal{X}(a,b) \leq \mathcal{Y}(F(a),F(b))\\). Using this and the fact that \\(- \otimes A\\) and \\(A \otimes -\\) are monotone, have:

\[ \mathcal{Y}(F(a), b) \otimes \mathcal{X}(c,a) \otimes \mathcal{Y}(b,d) \leq \mathcal{Y}(F(a), b) \otimes \mathcal{Y}(F(c),F(a)) \otimes \mathcal{Y}(b,d)\]

With this, we can show \\(\mathcal{Y}(F(a), b) \otimes \mathcal{X}(c,a) \otimes \mathcal{Y}(b,d) \leq \mathcal{Y}(F(c), d)\\) by applying condition (b) of the definition of a \\(\mathcal{V}\\)-enriched category from [Lecture 29](https://forum.azimuthproject.org/discussion/2121/lecture-29-chapter-2-enriched-categories), using commutativity, transitivity and the monotony of \\(\otimes\\) where necessary.