-A nat n is defined by what it can do, which is to compute a function iterated n times. In the polymorphic
-encoding above, the result of that iteration can be any type α, as long as you have a base element z : α and
-a function s : α → α.
+A nat n is defined by what it can do, which is to compute a function iterated n
+times. In the polymorphic encoding above, the result of that iteration can be
+any type 'a, as long as you have a base element z : 'a and a function s : 'a → 'a.