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} \$