(**Edit**: I had originally tried to prove this by assuming \$$x \leq y \iff x = y\$$. I have updated this proof to fully answer the puzzle based on Anindya's comments below.)

> **Puzzle 197.** Suppose \$$\mathcal{V}\$$ is a closed commutative monoidal poset and \$$\mathcal{X}\$$ is any \$$\mathcal{V}\$$-enriched category. Show that there is a \$$\mathcal{V}\$$-enriched functor, the **hom functor**
>
> $\mathrm{hom} \colon \mathcal{X}^{\text{op}} \times \mathcal{X} \to \mathcal{V}$
>
> defined on any object \$$(x,x') \$$ of \$$\mathcal{X}^{\text{op}} \times \mathcal{X} \$$ by
>
> $\mathrm{hom}(x,x') = \mathcal{X}(x,x') .$

**Proof.**

Going back to [Lecture 32](https://forum.azimuthproject.org/discussion/2169/lecture-32-chapter-2-enriched-functors), we have the following definition of a \$$\mathcal{V}\$$-functor.

> **Definition.** Let \$$\mathcal{X}\$$ and \$$\mathcal{Y}\$$ be \$$\mathcal{V}\$$-categories. A **\$$\mathcal{V}\$$-functor from \$$\mathcal{X}\$$ to \$$\mathcal{Y}\$$**, denoted \$$F\colon\mathcal{X}\to\mathcal{Y}\$$, is a function
>
> $F\colon\mathrm{Ob}(\mathcal{X})\to \mathrm{Ob}(\mathcal{Y})$
>
> such that
>
> $\mathcal{X}(x,x') \leq \mathcal{Y}(F(x),F(x')) \tag{X}$
>
> for all \$$x,x' \in\mathrm{Ob}(\mathcal{X})\$$.

We want \$$F = \mathrm{hom}\$$ and \$$\mathcal{Y} = \mathcal{V}\$$.

Based on [Lecture 60](https://forum.azimuthproject.org/discussion/2287/lecture-60-chapter-4-closed-monoidal-posets), to make \$$\mathrm{hom}\$$ a \$$\mathcal{V}\$$-enriched functor we want to make the action of \$$\mathcal{Y}\$$ on objects be \$$(a,b) \mapsto a \multimap b \$$.

All that is left is to prove \$$\mathrm{hom}\$$ satisfies the rules of a \$$\mathcal{V}\$$-enriched functor.

To see \$$\mathrm{hom} = \mathcal{X}\$$ works, we know:

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

Hence, using commutativity and the fact that \$$A \otimes - \dashv A \multimap - \$$, then \$$\text{(X)}\$$ says that \$$\mathrm{hom}\$$ is a \$$\mathcal{V}\$$-Functor if and only if:

$\begin{eqnarray} & (\mathcal{X}^{\text{op}} \times \mathcal{X})((a,b),(c,d)) \leq \mathrm{hom}(a,b) \multimap \mathrm{hom}(c,d) \\\\ & \iff \\\\ & \mathcal{X}(c,a) \otimes \mathcal{X}(b,d) \leq \mathrm{hom}(a,b) \multimap \mathrm{hom}(c,d) \\\\ & \iff \\\\ & \mathrm{hom}(a,b) \otimes \mathcal{X}(c,a) \otimes \mathcal{X}(b,d) \leq \mathrm{hom}(c,d) \\\\ & \iff \\\\ & \mathcal{X}(a,b) \otimes \mathcal{X}(c,a) \otimes \mathcal{X}(b,d) \leq \mathcal{X}(c,d) \\\\ & \iff \\\\ & \mathcal{X}(c,a) \otimes \mathcal{X}(a,b) \otimes \mathcal{X}(b,d) \leq \mathcal{X}(c,d) \tag{Y} \end{eqnarray}$

So it suffices to show \$$\text{(Y)}\$$. To do this, observe:

1. \$$- \otimes \mathcal{X}(x,y)\$$ is monotone for all \$$x\$$ and \$$y\$$, since \$$\mathcal{V}\$$ is a monoidal pre-order as defined in [Lecture 21](https://forum.azimuthproject.org/discussion/2082/lecture-21-chapter-2-monoidal-preorders)
2. \$$\mathcal{X}(x,y)\otimes\mathcal{X}(y,z)\leq\mathcal{X}(x,z)\$$; this is from condition (b) of the definition of a \$$\mathcal{V}\$$-enriched category in [Lecture 29](https://forum.azimuthproject.org/discussion/2121/lecture-29-chapter-2-enriched-categories)

From (2) we have

$\mathcal{X}(c,a) \otimes \mathcal{X}(a,b) \leq \mathcal{X}(c,b)$

This with (1) means

$\mathcal{X}(c,a) \otimes \mathcal{X}(a,b) \otimes \mathcal{X}(b,d) \leq \mathcal{X}(c,b) \otimes \mathcal{X}(b,d) \tag{★}$

But we also know from (2) that

$\mathcal{X}(c,b) \otimes \mathcal{X}(b,d) \leq \mathcal{X}(c,b)$

This along with (★) and transitivity shows \$$\mathcal{X}(c,a) \otimes \mathcal{X}(a,b) \otimes \mathcal{X}(b,d) \leq \mathcal{X}(c,d)\$$ as desired.
\$$\qquad \blacksquare \$$