re this puzzle:

> **Puzzle 210.** Show that \$$\Phi \otimes \Psi\$$ is really a feasibility relation if \$$\Phi\$$ and \$$\Psi\$$ are feasibility relations.

I thought it might be worth proving it in the general case, ie

$\Phi \text{ and } \Psi \text{ are }\mathcal{V}\text{-profunctors} \implies (\Phi\otimes\Psi) \text{ is a }\mathcal{V}\text{-profunctor}$

This amounts to proving that for all objects \$$(x, x')\$$ and \$$(a, a')\$$ in \$$X\times X'\$$, and all objects \$$(y, y')\$$ and \$$(b, b')\$$ in \$$Y\times Y'\$$, we have:

$(X\times X')((a, a'), (x, x')) \otimes (\Phi \otimes \Psi)((x, x'), (y, y')) \otimes (Y \times Y')((y, y'), (b, b')) \leq (\Phi \otimes \Psi)((a, a'), (b, b'))$

Using the definitions of \$$X\times X', \Phi \otimes \Psi, Y \times Y'\$$ we see that the left hand side is

$\big(X(a, x) \otimes X'(a', x')\big) \otimes \big(\Phi(x, y) \otimes \Psi(x', y')\big) \otimes \big(Y(y, b) \otimes Y(y', b')\big)$

We can reorder this because \$$\otimes\$$ is symmetric:

$\big(X(a, x) \otimes \Phi(x, y) \otimes Y(y, b)\big) \otimes \big(X'(a', x') \otimes \Psi(x', y') \otimes Y(y', b')\big)$

But \$$\Phi\$$ and \$$\Psi\$$ are \$$\mathcal{V}\$$-profunctors, and \$$\otimes\$$ is monotone, so this must be \$$\leq\$$

$\Phi(a, b) \otimes \Psi(a', b')$

... which is just the definition of \$$(\Phi \otimes \Psi)((a, a'), (b, b'))\$$. QED.