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