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.