David Lambert, we want ***Bool***-functors. This means that secretly we want monotone functions that have the poset **Bool** as the codomain.

This means that a **Bool**-profunctor,

\\[
X \nrightarrow Y
\\]

is secretly a monotone function,

\\[
X \otimes Y \to \mathbf{Bool}.
\\]

So for the inverse left unitor **Bool**-profunctor (say that 10-times fast),

\[ \lambda_\mathcal{X}^{-1} : X \nrightarrow 1\otimes X.\]

we actually have something like,

\\[
\lambda_{X}^{-1}: X\otimes(1\otimes X) \to \mathbf{Bool}
\\\\
\lambda_{X}^{-1}((x),(0,x)) = \begin{cases}
\texttt{true} & \text{ if } x \leq (0,x) \\\\
\texttt{false} & \text{otherwise}
\end{cases}
\\]