-different type! For instance, if zero has type σ, and `false`
-has type `τ --> τ --> τ` for some τ, and one is
-represented by the function `\x.x false 0`, then one must have type
-`(τ --> τ --> &tau) --> &sigma --> σ`. But this is a
-different type than zero! Because numbers have different types, it
-becomes impossible to write arithmetic operations that can combine
-zero with one. We would need as many different addition operations as
-we had pairs of numbers that we wanted to add.
+different type! For instance, if zero has type σ, then `false`
+has type τ --> τ --> &tau, for some τ. Since one is
+represented by the function `\x.x false 0`, one must have type `(τ
+--> τ --> &tau) --> &sigma --> σ`. But this is a different
+type than zero! Because each number has a different type, it becomes
+impossible to write arithmetic operations that can combine zero with
+one. We would need as many different addition operations as we had
+pairs of numbers that we wanted to add.