Christopher: I was asking Keith to define

$\Phi \colon \textbf{Bool}^{\text{op}} \times [0,\infty) \to \textbf{Bool}$

and check that _this_ is a monotone function.

But yeah, we are not looking for a monotone function \$$\Phi \colon \textbf{Bool} \to [0,\infty) \$$. A monotone function \$$\Phi \colon \textbf{Bool}^{\text{op}} \times [0,\infty) \to \textbf{Bool} \$$ is the same as a relation from \$$\textbf{Bool}\$$ to \$$[0,\infty)\$$ that obeys certain properties:

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

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