>**Puzzle 198.** Suppose \\(\mathcal{V}\\) is a commutative quantale, and suppose
>\\( \Phi \colon \mathcal{X}^{\text{op}} \times \mathcal{Y} \to \mathcal{V} \\) and \\( \Psi \colon \mathcal{Y}^{\text{op}} \times \mathcal{Z} \to \mathcal{V} \\) are \\(\mathcal{V}\\)-enriched functors. Show that \\( \Psi\Phi \colon \mathcal{X}^{\text{op}} \times \mathcal{Y} \to \mathcal{V} \\), defined by

>\[ (\Psi\Phi)(x,z) = \bigvee_{y \in Y} \Phi(x,y) \otimes \Psi(y,z),\]

>is a \\(\mathcal{V}\\)-enriched functor. There are two axioms to check - you can find them in [Lecture 32](https://forum.azimuthproject.org/discussion/2169/lecture-32-chapter-2-enriched-functors/p1).

We need to check:

1. \\(\Psi\Phi: Ob(\mathcal{X^{op}} \times \mathcal{Z}) \rightarrow Ob(\mathcal{V})\\)
2. \\((\mathcal{X}^{op} \times \mathcal{Z})(x_1, z_1), (x_2, z_2)) \leq \mathcal{V}(\Psi\Phi(x_1, z_1), \Psi\Phi(x_2, z_2))\\)


**1. \\(\Psi\Phi: Ob(\mathcal{X^{op}} \times \mathcal{Z}) \rightarrow Ob(\mathcal{V})\\)**

We are given:
\[\Phi : Ob(\mathcal{X^{op}} \times \mathcal{Y}) \rightarrow Ob(\mathcal{V})\]
\[\Psi : Ob(\mathcal{Y^{op}} \times \mathcal{Z}) \rightarrow Ob(\mathcal{V})\]

First we compose the two:

\[\Psi\Phi : Ob(\mathcal{Y^{op}} \times \mathcal{Z}) \rightarrow Ob(\mathcal{X^{op}} \times \mathcal{Y}) \rightarrow Ob(\mathcal{V})\]

We can switch the order using opposite categories:
\[\Psi\Phi : Ob(\mathcal{Z^{op}} \times \mathcal{Y}) \rightarrow Ob( \mathcal{Y^{op}} \times \mathcal{X}) \rightarrow Ob(\mathcal{V})\]

Then by currying :
\[\Psi\Phi : \mathcal{Z^{op}} \rightarrow \mathcal{Y} \rightarrow \mathcal{Y^{op}} \rightarrow \mathcal{X} \rightarrow Ob(\mathcal{V})\]

By transitivity:
\[\Psi\Phi : \mathcal{Z^{op}} \rightarrow \mathcal{X} \rightarrow Ob(\mathcal{V})\]

Curry back out and switch the order using opposites:
\[\Psi\Phi: Ob(\mathcal{X^{op}} \times \mathcal{Z}) \rightarrow Ob(\mathcal{V})\]



**2. \\((\mathcal{X}^{op} \times \mathcal{Z})(x_1, z_1), (x_2, z_2)) \leq \mathcal{V}(\Psi\Phi(x_1, z_1), \Psi\Phi(x_2, z_2))\\)**

Since \\(\Phi\\) and \\(\Psi\\) are \\(\mathcal{V}\\)-enriched functors, using our "profunctor rule" we have:
\[\mathcal{X}(x_2, x_1) \otimes \Phi(x_1, y_1) \otimes \mathcal{Y}(y_1, y_2) \leq \Phi(x_2, y_2)\]
\[\mathcal{Y}(Y_2, y_1) \otimes \Psi(y_1, z_1) \otimes \mathcal{Z}(z_1, z_2) \leq \Psi(y_2, z_2)\]

Then we can combine these two:
\[\mathcal{X}(x_2, x_1) \otimes \Phi(x_1, y_1) \otimes \mathcal{Y}(y_1, y_2) \otimes \mathcal{Y}(y_2, y_1) \otimes \Psi(y_1, z_1) \otimes \mathcal{Z}(z_1, z_2) \leq \Phi(x_2, y_2) \otimes \Psi(y_2, z_2)\]

\\(\mathcal{Y}(y_1, y_2) \otimes \mathcal{Y}(y_2, y_1)\\) cancels out since we are going back and forth:
\[\mathcal{X}(x_2, x_1) \otimes \Phi(x_1, y_1) \otimes \Psi(y_1, z_1) \otimes \mathcal{Z}(z_1, z_2) \leq \Phi(x_2, y_2) \otimes \Psi(y_2, z_2)\]

Then by definition of profunctor composition, we can combine \\(\Phi\\) and \\(\Psi\\) terms:
\[\mathcal{X}(x_2, x_1) \otimes \Psi\Phi(x_1, z_1) \otimes \mathcal{Z}(z_1, z_2) \leq \Psi\Phi(x_2, z_2)\]

Since \\(\mathcal{V}\\) is commutative and closed, we get:
\[\mathcal{X}(x_2, x_1) \otimes \mathcal{Z}(z_1, z_2) \leq \Psi\Phi(x_1, z_1) \multimap \Psi\Phi(x_2, z_2)\]

By definition of product category given in [Lecture 62](https://forum.azimuthproject.org/discussion/2292/lecture-62-chapter-4-constructing-enriched-categories#latest):
\[(\mathcal{X}^{op} \times \mathcal{Z})(x_1, z_1), (x_2, z_2)) \leq \Psi\Phi(x_1, z_1) \multimap \Psi\Phi(x_2, z_2)\]

By definition of \\(\mathcal{V}\\) being a closed monoidal preorder:
\[(\mathcal{X}^{op} \times \mathcal{Z})(x_1, z_1), (x_2, z_2)) \leq \mathcal{V}(\Psi\Phi(x_1, z_1), \Psi\Phi(x_2, z_2))\]