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

Hence:

\begin{align} (\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)\ . \end{align}

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.