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}\\).