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'.