John Baez wrote:

> Really? Huh, maybe so! It seemed so obvious to me that this feasibility relation was the *conjoint* of a function. Are both of us right? Neither? Just one of us?

Let me try to justify myself and we can see where I'm going off the rails.

In Lecture 65, you wrote approximately:

> Any \$$\mathcal{V}\$$-enriched functor \$$F: \mathcal{X} \to \mathcal{Y}\$$ gives a \$$\mathcal{V}\$$-enriched profunctor
>
> $\hat{F} \colon \mathcal{X} \nrightarrow \mathcal{Y}$
>
> defined by
>
> $\hat{F} (x,y) = \mathcal{Y}(F(x), y ) .$
>
> \$$\hat{F} \colon \mathcal{X} \nrightarrow \mathcal{Y}\$$ is called the **companion** of \$$F\$$.

In this case \$$\mathcal{X} = \mathbf{Bool}\$$ and \$$\mathcal{Y} = [0,\infty)\$$. So let \$$F\$$ map \$$\mathtt{false} \mapsto 0\$$ and \$$\mathtt{true} \mapsto 500\$$. Then \$$\hat{F}(x,y) = F(x) \leq y\$$.

But \$$\hat{F}\$$ is the same as Dan Oneata's answer! Let's check that. First let \$$x = \mathtt{false}\$$:

\begin{align} \hat{F}(\mathtt{false},y) & = F(\mathtt{false}) \leq y \\\\ & = 0 \leq y \\\\ & = \mathtt{true} \end{align}

So \$$\hat{F}(\mathtt{false},y) = \mathtt{true} \text{, for all } y \in [0,\infty)\$$ ✔

Next, consider:

\begin{align} \hat{F}(\mathtt{true},y) & = F(\mathtt{true}) \leq y \\\\ & = 500 \leq y \end{align}

If \$$500 \leq y\$$, then \$$\hat{F}(\mathtt{true},y)\$$ is \$$\mathtt{true}\$$. Otherwise, \$$\hat{F}(\mathtt{true},y)\$$ is \$$\mathtt{false}\$$.

But that's just the same as saying \$$\hat{F}(\texttt{true}, y) = \begin{cases} \texttt{true} &\mbox{if } 500 \le y \\\\ \texttt{false} & \mbox{otherwise.}\end{cases}\$$ ✔

Hopefully I haven't misunderstood how companions are defined...