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