Yoav - yes, you're right!

In Puzzle 209, \\(\Phi, \Psi \colon \mathbf{N} \to \mathbf{N}\\) are both the identity feasibility relation, and we are tensoring them and getting the identity feasibility relation from \\(\mathbb{N} \times \mathbb{N}\\) to itself.

If anyone doesn't see why these guys are identities, they can look at [Lecture 64](https://forum.azimuthproject.org/discussion/2298/lecture-64-chapter-4-the-category-of-enriched-profunctors#latest), where I proved this:

> **Lemma.** For any \\(\mathcal{V}\\)-enriched category \\(\mathcal{X}\\), 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.

A feasibility relation is just a \\(\textbf{Bool}\\)-enriched profunctor, so we can water down the above Lemma to this special case:

**Watered-Down Lemma.** For an preorder \\(X\\), the monotone function \\( \mathrm{hom} \colon X^{\text{op}} \times X \to \mathbf{Bool} \\), defined by

\[ \mathrm{hom}(x,x') =

\begin{cases}

\texttt{true} & \mbox{if } x \le x' \\\\

\texttt{false} & \mbox{otherwise.}

\end{cases}

\]

corresponds to a feasibility relation

\[ 1\_{\mathcal{X}} \colon X \nrightarrow X \]

that serves as an identity for composition.

In [Lecture 67](https://forum.azimuthproject.org/discussion/2303/lecture-67-chapter-4-collaborative-design/p1) we'll see another use for the 'hom-functor': it not only gives identities, it gives something called the 'cup'.

In Puzzle 209, \\(\Phi, \Psi \colon \mathbf{N} \to \mathbf{N}\\) are both the identity feasibility relation, and we are tensoring them and getting the identity feasibility relation from \\(\mathbb{N} \times \mathbb{N}\\) to itself.

If anyone doesn't see why these guys are identities, they can look at [Lecture 64](https://forum.azimuthproject.org/discussion/2298/lecture-64-chapter-4-the-category-of-enriched-profunctors#latest), where I proved this:

> **Lemma.** For any \\(\mathcal{V}\\)-enriched category \\(\mathcal{X}\\), 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.

A feasibility relation is just a \\(\textbf{Bool}\\)-enriched profunctor, so we can water down the above Lemma to this special case:

**Watered-Down Lemma.** For an preorder \\(X\\), the monotone function \\( \mathrm{hom} \colon X^{\text{op}} \times X \to \mathbf{Bool} \\), defined by

\[ \mathrm{hom}(x,x') =

\begin{cases}

\texttt{true} & \mbox{if } x \le x' \\\\

\texttt{false} & \mbox{otherwise.}

\end{cases}

\]

corresponds to a feasibility relation

\[ 1\_{\mathcal{X}} \colon X \nrightarrow X \]

that serves as an identity for composition.

In [Lecture 67](https://forum.azimuthproject.org/discussion/2303/lecture-67-chapter-4-collaborative-design/p1) we'll see another use for the 'hom-functor': it not only gives identities, it gives something called the 'cup'.