Since the puzzles from [last time](https://forum.azimuthproject.org/discussion/2295/lecture-63-chapter-4-composing-enriched-profunctors#latest) were quite substantial, let me copy the nice solutions provided by Anindya Bhattyacharyya and Matthew Doty here. They add up to the proof of this:

**Theorem.** Suppose \$$\mathcal{V}\$$ is a commutative quantale. Then there is a category \$$\mathbf{Prof}_\mathcal{V}\$$ whose objects are \$$\mathcal{V}\$$-enriched categories and whose morphisms are \$$\mathcal{V}\$$-enriched profunctors, where the composite of \$$\mathcal{V}\$$-enriched profunctors \$$\Phi \colon \mathcal{X} \nrightarrow \mathcal{Y} \$$ and \$$\Psi \colon \mathcal{Y} \to \mathcal{Z}\$$ is defined by

$(\Psi\Phi)(x,z) = \bigvee_{y \in \mathrm{Ob}(\mathcal{Y})} \Phi(x,y) \otimes \Psi(y,z).$

We'll break the proof into lots of lemmas. In all that follows, \$$\mathcal{V}\$$ is a commutative quantale and \$$\mathcal{W}, \mathcal{X}, \mathcal{Y}, \mathcal{Z}\$$ are \$$\mathcal{V}\$$-enriched categories. Letters like \$$w,w',x,x',y,y',z,z'\$$ will always stand for objects in the enriched categories with the same letters as their names - and when I write inequalities involving these I mean they're true _for all choices_ of these objects, unless I say otherwise.

First we check that the formula above really defines a \$$\mathcal{V}\$$-enriched profunctor!

**Lemma.** Suppose \$$\Phi \colon \mathcal{X} \nrightarrow \mathcal{Y} \$$ and \$$\Psi \colon \mathcal{Y} \to \mathcal{Z}\$$ are \$$\mathcal{V}\$$-enriched profunctors. Then the formula

$(\Psi\Phi)(x,z) = \bigvee_{y} \Phi(x,y) \otimes \Psi(y,z)$

specifies a \$$\mathcal{V}\$$-enriched profunctor \$$\Psi\Phi \colon \mathcal{X} \to \mathcal{Y}\$$.

**Proof.** We need to show that

$\Psi\Phi \colon \mathcal{X}^{\text{op}} \times \mathcal{Z} \to \mathcal{V}$

is a \$$\mathcal{V}\$$-enriched functor, meaning

$(\mathcal{X}^\text{op}\times \mathcal{Z})((x, z), (x', z')) \leq \mathcal{V}(\Psi\Phi)(x, z), (\Psi\Phi)(x', z'))$

or in other words

$\mathcal{X}(x', x) \otimes \mathcal{Z}(z, z') \leq (\Psi\Phi)(x, z)\multimap(\Psi\Phi)(x', z') .$

Using the definitions this becomes

$\mathcal{X}(x', x) \otimes \left(\bigvee_y \Phi(x, y)\otimes\Psi(y, z)\right) \otimes\mathcal{Z}(z, z') \leq \bigvee_y \Phi(x', y)\otimes\Psi(y, z')$

or since \$$\otimes\$$ distributes over \$$\bigvee\$$ in a quantale,

$\bigvee_y \mathcal{X}(x', x) \otimes \Phi(x, y)\otimes\Psi(y, z) \otimes\mathcal{Z}(z, z') \leq \bigvee_y \Phi(x', y)\otimes\Psi(y, z').$

This is true because

$\mathcal{X}(x', x) \otimes \Phi(x, y) \le \Phi(x',y)$

and

$\Psi(y, z) \otimes\mathcal{Z}(z, z') \le \Phi(y,z')$

by the following theorem. \$$\qquad \blacksquare \$$

This is a very handy tool:

**Theorem.** The following are equivalent:

1. \$$\Phi : \mathcal{X} \nrightarrow \mathcal{Y}\$$ is a \$$\mathcal{V}\$$-enriched profunctor.

2. \$$\mathcal{X}(x', x) \otimes \Phi(x, y) \otimes \mathcal{Y}(y, y') \leq \Phi(x',y')\$$ for all \$$x,x',y,y'\$$.

3. \$$\mathcal{X}(x', x) \otimes \Phi(x, y) \leq \Phi(x', y)\$$ and \$$\Phi(x, y) \otimes \mathcal{Y}(y, y') \leq \Phi(x, y')\$$ for all \$$x,x',y,y'\$$.

**Proof.** Item 1 is true iff \$$\Phi : \mathcal{X}^\text{op} \times \mathcal{Y} \to \mathcal{V}\$$ is a \$$\mathcal{V}\$$-functor, which by definition is true iff

$(\mathcal{X}^\text{op} \times \mathcal{Y})((x, y), (x', y')) \leq \mathcal{V}(\Phi(x, y), \Phi(x',y'))$

for all \$$x,x',y,y'\$$. Using the definitions, this is equivalent to

$\mathcal{X}(x', x) \otimes \mathcal{Y}(y, y') \leq \Phi(x, y) \multimap \Phi(x', y') .$

By the definition of\$$\multimap\$$ this in turn is equivalent to

$\Phi(x, y) \otimes \mathcal{X}(x', x) \otimes \mathcal{Y}(y, y') \leq \Phi(x', y')$

Because \$$\otimes\$$ is commutative this is the same as item 2. Thus, 1 is equivalent to 2.

Next note that \$$I \leq \mathcal{X}(x, x)\$$ and \$$I \leq \mathcal{Y}(y, y)\$$ by the definition of a \$$\mathcal{V}\$$-category. Thus, given 2 we can set \$$y' = y\$$ to get

$\mathcal{X}(x', x) \otimes \Phi(x, y) = \mathcal{X}(x', x) \otimes \Phi(x, y) \otimes I \leq \mathcal{X}(x', x) \otimes \Phi(x, y) \otimes \mathcal{Y}(y, y) \leq \Phi(x', y)$

or we can set \$$x' = x\$$ to get

$\Phi(x, y) \otimes \mathcal{Y}(y, y') = I \otimes \Phi(x, y) \otimes \mathcal{Y}(y, y') \leq \mathcal{X}(x, x) \otimes \Phi(x, y) \otimes \mathcal{Y}(y, y') \leq \Phi(x, y')$

Thus, 2 implies 3. On the other hand, using 3 we can show 2:

$\mathcal{X}(x', x) \otimes \Phi(x, y) \otimes \mathcal{Y}(y, y') \leq \Phi(x', y) \otimes \mathcal{Y}(y, y') \leq \Phi(a, b)$

Thus, all three conditions are equivalent. \$$\qquad \blacksquare \$$

Next we check that composition is associative:

**Lemma.** Suppose \$$\Theta \colon \mathcal{W} \nrightarrow \mathcal{X}, \Phi \colon \mathcal{X} \nrightarrow \mathcal{Y} \$$ and \$$\Psi \colon \mathcal{Y} \to \mathcal{Z}\$$ are \$$\mathcal{V}\$$-enriched profunctors. Then

$(\Psi \Phi) \Theta = \Psi (\Phi \Theta) .$

**Proof.** We need to show

$\bigvee_{x} \Theta(x,y) \otimes \left( \bigvee_{y} \Phi(x,y) \otimes \Psi(y,z) \right) = \bigvee_{y} \left( \bigvee_{x} \Theta(x,y) \otimes \Phi(x,y) \right) \otimes \Psi(y,z) .$

Because \$$\otimes\$$ distributes over \$$\bigvee\$$, it's enough to show

$\bigvee_{x} \bigvee_{y} \Theta(x,y) \otimes \left( \Phi(x,y) \otimes \Psi(y,z) \right) = \bigvee_{y} \bigvee_{x} \Theta(x,y) \otimes \Phi(x,y) \otimes \Psi(y,z) .$

Since \$$\otimes\$$ is associative, and we always have \$$\bigvee_{x} \bigvee_{y} = \bigvee_{y} \bigvee_{x} \$$ when the joins in question exist, this is true. \$$\qquad \blacksquare \$$

Next we show our would-be category \$$\mathbf{Prof}_\mathcal{V}\$$ has identity morphisms.

**Lemma.** The \$$\mathcal{V}\$$-enriched functor \$$\mathrm{hom} \colon \mathcal{X}^{\text{op}} \times \mathcal{X} \to \mathcal{V} \$$, defined by

$\mathrm{hom}(x,x') = \mathcal{X}(x,x') ,$

corresponds to a \$$\mathcal{V}\$$-enriched profunctor

$1\_{\mathcal{X}} \colon \mathcal{X} \nrightarrow \mathcal{X}$

that serves as an identity for composition.

**Proof.** We need to check the left and right unit laws, but they are very similar so we'll only do one:

$\Phi 1_{\mathcal{X}} = \Phi$

for any \$$\mathcal{V}\$$-enriched profunctor \$$\Phi \colon \mathcal{X} \to \mathcal{Y}\$$. This amounts to proving

$\bigvee_{x'} \mathcal{X}(x,x') \otimes \Phi(x',y) = \Phi(x,y)$

First we'll show

$\Phi(x,y) \le \bigvee_{x'} \mathcal{X}(x,x') \otimes \Phi(x',y)$

and then we'll show the reverse inequality. Since \$$\mathcal{V}\$$ is a poset this will mean the two sides are equal.

For the inequality above it's enough to find one choice of \$$x'\$$ that makes

$\Phi(x,y) \le \mathcal{X}(x,x') \otimes \Phi(x',y) .$

The obvious guess is \$$x' = x\$$; then we need

$\Phi(x,y) \le \mathcal{X}(x,x) \otimes \Phi(x,y) .$

But the [definition of enriched category](https://forum.azimuthproject.org/discussion/2121/lecture-29-chapter-2-enriched-categories/p1) says that \$$I \le \mathcal{X}(x,x)\$$, so

$\Phi(x,y) = I \otimes \mathcal{\Phi}(x,y) \le \mathcal{X}(x,x) \otimes \Phi(x,y)$

as desired. Next we show the reverse inequality:

$\bigvee_{x'} \mathcal{X}(x,x') \otimes \Phi(x',y) \le \Phi(x,y) .$

For this it's enough to prove that for _all_ \$$x'\$$ we have

$\mathcal{X}(x,x') \otimes \Phi(x',y) \le \Phi(x,y) .$

We've seen this in the theorem above, so we're done. \$$\qquad \blacksquare \$$

Whew - that was a good workout! #:-S

**[To read other lectures go here.](http://www.azimuthproject.org/azimuth/show/Applied+Category+Theory#Chapter_4)**