Okay, this ended up being a lot tougher than I was hoping, but here's my attempted proof of **Puzzle 200**.

> **Puzzle 200.** Suppose that \\(\mathcal{V}\\) is a commutative quantale and \\(\mathcal{X}\\) is a \\(\mathcal{V}\\)-enriched category. The hom-functor
>
> \[ \mathrm{hom} : \mathcal{X}^{\text{op}} \times \mathcal{X} \to \mathcal{V} \]
>
> described in [Puzzle 197](https://forum.azimuthproject.org/discussion/2292/lecture-62-chapter-4-constructing-enriched-categories/p1) gives an enriched profunctor that we call \\(1_{\mathcal{V}} \colon \mathcal{V} \to \mathcal{V}\\). Show that this serves as an identity for composition of \\(\mathcal{V}\\)-enriched profunctors: check the left and right unit laws.

Let \\(\Phi : \mathcal{A} \nrightarrow \mathcal{B} \\) be a \\(\mathcal{V}\\)-profunctor, and let \\(1_{\mathcal{A}} : \mathcal{A} \nrightarrow \mathcal{A} \\) and \\(1_{\mathcal{B}} : \mathcal{B} \nrightarrow \mathcal{B} \\) be \\(\mathcal{V}\\)-profunctors such that \\(1_{\mathcal{A}}(x,y) = \mathcal{A}(x,y)\\) and \\(1_{\mathcal{B}}(x,y) = \mathcal{B}(x,y)\\) .

We want to show \\(1_{\mathcal{A}} \Phi = \Phi 1_{\mathcal{B}} = \Phi \\). Expanding the definition of \\(\mathcal{V}\\)-profunctor composition and the definitions of \\(1_{\mathcal{A}}\\) and \\(1_{\mathcal{B}}\\), we need to show:

\[
\bigvee_{x \in \mathrm{obj}(\mathcal{A})} \left( \mathcal{A}(a,x) \otimes \Phi(x,b) \right) = \bigvee_{y \in \mathrm{obj}(\mathcal{B})} \left( \Phi(a,y) \otimes \mathcal{B}(y,b) \right) = \Phi(a,b)
\]

I am only going to show \\(
\bigvee_{x \in \mathrm{obj}(\mathcal{A})} \left( \mathcal{A}(a,x) \otimes \Phi(x,b) \right) = \Phi(a,b)
\\), since the argument for the other identity is symmetrical.

In [comment 18](https://forum.azimuthproject.org/discussion/comment/20194/#Comment_20194) in Lecture 62 Anindya Bhattacharyya identified a nice rule: if \\(\mathcal{V}\\) is a commutative quantale then
\[ \Phi: \mathcal{A} \nrightarrow \mathcal{B} \text{ is a } \mathcal{V} \text{-profunctor} \iff \mathcal{A}(a, x) \otimes \Phi(x, y) \otimes \mathcal{B}(y, b) \leq \Phi(a, b) \text{ for all } a, x, y, b \tag{A}\]

Since \\(\mathcal{B}\\) is a \\(\mathcal{V}\\)-category we know \\(I \leq \mathcal{B}(b,b)\\). Using the monotony of \\((x \otimes -)\\) that John proved in [#6](https://forum.azimuthproject.org/discussion/comment/20236/#Comment_20236), \\(x \otimes I = x\\) and (A) we have for all \\(a\\), \\(x\\) and \\(b\\)

\[
\mathcal{A}(a,x) \otimes \Phi(x,b) \leq \mathcal{A}(a,x) \otimes \Phi(x,b) \otimes \mathcal{B}(b,b) \leq \Phi(a,b)
\]

Since this holds for all \\(x\\), we may introduce a supremum:

\[
\bigvee_{x \in \mathrm{obj}(\mathcal{A})}\mathcal{A}(a,x) \otimes \Phi(x,b) \leq \Phi(a,b) \tag{B}
\]

Moreover, since \\(\mathcal{A}\\) is a \\(\mathcal{V}\\)-category we have \\(I \leq \mathcal{A}(a,a)\\). Using this and the identity laws, commutativity and the monotony of \\((x \otimes -)\\) we have
\[
\Phi(a,b) \leq \mathcal{A}(a,a) \otimes \Phi(a,b) \tag{C}
\]

But also notice

\[
\mathcal{A}(a,a) \otimes \Phi(a,b) \in \lbrace \mathcal{A}(a,x) \otimes \Phi(x,b)\ \mid\ x \in \mathrm{obj}(\mathcal{A}) \rbrace
\]

hence

\[
\mathcal{A}(a,a) \otimes \Phi(a,b) \leq \bigvee \lbrace \mathcal{A}(a,x) \otimes \Phi(x,b)\ \mid\ x \in \mathrm{obj}(\mathcal{A}) \rbrace
\]

However \\(\bigvee_{x \in \mathrm{obj}(\mathcal{A})}\mathcal{A}(a,x) \otimes \Phi(x,b)\\) is really just syntactic sugar for \\(\bigvee \lbrace \mathcal{A}(a,x) \otimes \Phi(x,b)\ \mid\ x \in \mathrm{obj}(\mathcal{A}) \rbrace\\). Using the nicer notation, we have:

\[
\mathcal{A}(a,a) \otimes \Phi(a,b) \leq \bigvee_{x \in \mathrm{obj}(\mathcal{A})}\mathcal{A}(a,x) \otimes \Phi(x,b)
\]

with (C) we have

\[
\Phi(a,b) \leq \bigvee_{x \in \mathrm{obj}(\mathcal{A})}\mathcal{A}(a,x) \otimes \Phi(x,b) \tag{D}
\]

From (B) and (D) it follows that \\(\bigvee_{x \in \mathrm{obj}(\mathcal{A})} \left( \mathcal{A}(a,x) \otimes \Phi(x,b) \right) = \Phi(a,b)\\) as desired \\( \qquad \blacksquare \\)