But a natural number can be viewed as a function from the natural numbers to {0, 1} via its binary expansion.

There's a trivial isomorphism between the natural numbers and binary sequences with finitely many ones, so a predicate of type `nat -> bool` can be viewed as a predicate of type `(nat -> bool) -> bool`.