Reuben wrote:

> Also, there seems to be analogy between treating functors of type (XxY->2) as morphisms in a new category and the lower level phenomenon of treating functions of type (XxY->2) as morphisms in a new category (Rel).

Yes! This is one of many instances of how the same patterns keep reappearing in richer and richer ways as one advances deeper into category theory.

An easy way to think about this is that any set can be reinterpreted as **discrete** poset, meaning one where \\(x\le y\\) iff \\(x = y\\).

A monotone function (or in other words, a \\(\textbf{Bool}\\)-enriched profunctor) between _discrete_ posets is just a function between the sets they came from.

A feasibility relation (or in other words, a \\(\textbf{Bool}\\)-enriched profunctor) between _discrete_ posets is just a relation between the sets they came from.

Category theorists would phrase this last fact as follows: there's a [full and faithful functor](https://en.wikipedia.org/wiki/Full_and_faithful_functors) from the category \\(\mathbf{Rel}\\) into the category of \\(\mathbf{Bool}\\)-enriched profunctors.

> Also, there seems to be analogy between treating functors of type (XxY->2) as morphisms in a new category and the lower level phenomenon of treating functions of type (XxY->2) as morphisms in a new category (Rel).

Yes! This is one of many instances of how the same patterns keep reappearing in richer and richer ways as one advances deeper into category theory.

An easy way to think about this is that any set can be reinterpreted as **discrete** poset, meaning one where \\(x\le y\\) iff \\(x = y\\).

A monotone function (or in other words, a \\(\textbf{Bool}\\)-enriched profunctor) between _discrete_ posets is just a function between the sets they came from.

A feasibility relation (or in other words, a \\(\textbf{Bool}\\)-enriched profunctor) between _discrete_ posets is just a relation between the sets they came from.

Category theorists would phrase this last fact as follows: there's a [full and faithful functor](https://en.wikipedia.org/wiki/Full_and_faithful_functors) from the category \\(\mathbf{Rel}\\) into the category of \\(\mathbf{Bool}\\)-enriched profunctors.