-this version of predecessor.
-
-Could we try to build a system for doing Church arithmetic in which
-the type for numbers always manipulated ordered pairs? The problem is
-that the ordered pairs we need here are pairs of numbers. If we tried
-to replace the type for Church numbers with a concrete (simple) type,
-we would have to replace each `X` with the type for Pairs, `(N -> N ->
-N) -> N`. But then we'd have to replace each of these `N`'s with the
-type for Church numbers, `(α -> α) -> α -> α`. And then we'd have to
-replace each of these `α`'s with... ad infinitum. If we had to choose
-a concrete type built entirely from explicit base types, we'd be
-unable to proceed.
+this version of computing the predecessor function.
+
+Could we try to accommodate the needs of the predecessor function by
+building a system for doing Church arithmetic in which the type for
+numbers always manipulated ordered pairs? The problem is that the
+ordered pairs we need here are pairs of numbers. If we tried to
+replace the type for Church numbers with a concrete (simple) type, we
+would have to replace each `N` with the type for Pairs, `(N -> N -> N)
+-> N`. But then we'd have to replace each of these `N`'s with the
+type for Church numbers, which we're imagining is `(Pair -> Pair) ->
+Pair -> Pair`. And then we'd have to replace each of these `Pairs`'s
+with... ad infinitum. If we had to choose a concrete type built
+entirely from explicit base types, we'd be unable to proceed.