Let's start trying to understand enriched profunctors. We'll start with a very nice special case: 'feasibility relations'.

**Definition.** Suppose \$$(X, \le_X) \$$ and \$$(Y, \le_Y) \$$ are preorders. Then a **feasibility relation** from \$$X\$$ to \$$Y\$$ is a monotone function

$\Phi : X^{\text{op}} \times Y \to \mathbf{Bool} .$

If \$$\Phi\$$ is a feasibility relation from \$$X\$$ to \$$Y\$$ we write \$$\Phi : X\nrightarrow Y \$$. If \$$\Phi(x,y) = \text{true}\$$, we say **\$$x\$$ can be obtained given \$$y\$$**.

The idea is that we use elements of \$$X\$$ to describe 'requirements' - things you want - and elements of \$$Y\$$ to describe 'resources' - things you have. A feasibility relation \$$\Phi : X \nrightarrow Y \$$ says when what you want can be obtained from what you have! And the fact that it's _monotone_ makes a lot of sense.

In fact:

**Theorem.** A function \$$\Phi : X^{\text{op}} \times Y \to \mathbf{Bool}\$$ is a feasibility relation if and only if:

1. If \$$\Phi(x,y) = \text{true}\$$ and \$$x' \le_X x\$$ then \$$\Phi(x',y) = \text{true}\$$.

2. If \$$\Phi(x,y) = \text{true}\$$ and \$$y \le_Y y'\$$ then \$$\Phi(x,y') = \text{true}\$$.

Translating this into English, we see it makes perfect sense:

1. If what you want can be obtained from the resources you have, and then you change your mind and want _less_, you can still obtain what you want.

2. If what you want can be obtained from the resources you have, and then you acquire _more_ resources, you can still obtain what you want.

But let's prove the theorem. This is mainly a nice review of various concepts.

**Proof.** First, remember that \$$\textbf{Bool}\$$ is the preorder with two elements \$$\text{true}\$$ and \$$\text{false}\$$, with

$\text{false} \le \text{true} .$

We can read \$$\le\$$ here as 'implies'.

Second, remember that \$$X^{\text{op}}\$$ is the **opposite** of the preorder \$$X\$$, with the definition of \$$\le\$$ turned around:

$x \le_{X^{\text{op}}} x' \text{ if and only if } x' \le_X x$

Third, remember that \$$X^{\text{op}} \times Y \$$ is the **product** of the preorders \$$X^{\text{op}}\$$ and \$$Y\$$. So, its elements are pairs \$$(x,y) \$$ with \$$x \in X\$$ and \$$y \in Y\$$, and we define a concept of \$$\le\$$ on these pairs by

$(x,y) \le (x',y') \text{ if and only if } x' \le_X x \text{ and } y \le_Y y' .$

Note how I said \$$x' \le x\$$. This looks backwards, but it's not one of my usual typos! It works this way because of the \$$\text{op}\$$ in
\$$X^{\text{op}} \times Y \$$.

Now we're ready to see exactly what a feasibility relation, that is a monotone function \$$\Phi : X^{\text{op}} \times Y \to \mathbf{Bool}\$$, really is. It's a function that obeys

$(x,y) \le (x',y') \text{ implies } \Phi(x,y) \le \Phi(x',y')$

or in other words

$\text{ if } x' \le_X x \text{ and } y \le_Y y', \text{ then } \Phi(x,y) \text{ implies } \Phi(x',y')$

Translating this into English to see what this means, it says:

> If you can get what you want from the resources you have, and then you change your mind and want _less_, and also go out and get _more_ resources, then you can still get what you want.

Here "less" really means "less than or equal to", and "more" really means "greater than or equal to" - English is not very good at saying these things quickly! So, the process of wanting less and getting more resources can always be broken into two steps:

1. wanting less but keeping the resources the same, and then

2. getting more resources but wanting the same thing.

So, this condition

$\text{ if } x' \le_X x \text{ and } y \le_Y y', \text{ then } \Phi(x,y) \text{ implies } \Phi(x',y')$

is equivalent to _the combination of both_ these conditions:

1. If \$$x' \le_X x \$$, then \$$\Phi(x,y) \$$ implies \$$\Phi(x',y)\$$.

2. If \$$y \le y'\$$, then \$$\Phi(x,y) \$$ implies \$$\Phi(x,y')\$$.

But here's another equivalent way to say these two things:

1. If \$$\Phi(x,y) = \text{true}\$$ and \$$x' \le_X x\$$ then \$$\Phi(x',y) = \text{true}\$$.

2. If \$$\Phi(x,y) = \text{true}\$$ and \$$y \le_X y'\$$ then \$$\Phi(x,y') = \text{true}\$$.

Logic! Ain't it great? \$$\qquad \blacksquare \$$

Next time I'll show you how to draw pictures of feasibility relations, and look at some examples. We've already drawn pictures of preorders, or at least posets: they're called **[Hasse diagrams](https://en.wikipedia.org/wiki/Hasse_diagram)**, and they look like a bunch of dots, one for each element of our poset \$$X\$$, and a bunch of arrows, enough so that \$$x \le y\$$ whenever there's a path of arrows leading from \$$x \$$ to \$$y \$$. So, to draw a feasibility
relation \$$\Phi : X \nrightarrow Y\$$, we'll draw two Hasse diagrams and some extra arrows to say when \$$\Phi(x,y) = \text{true}\$$.

Finally, two puzzles:

**Puzzle 169.** I gave a verbal argument for how we can break up any inequality \$$(x,y) \le (x',y') \$$ in \$$X^{\text{op}} \times Y\$$ into two other inequalities. Can you write this out in a purely mathematical way?

**Puzzle 170.** What if we have a morphism in a product of categories \$$\mathcal{C} \times \mathcal{D}\$$. Can we always write it as a composite of two morphisms, copying the procedure in my verbal argument and Puzzle 169? How does this work?

**[To read other lectures go here.](http://www.azimuthproject.org/azimuth/show/Applied+Category+Theory#Chapter_4)**