\x. f (g x)
+For example, the operation that maps a number `n` to <code>n<sup>2</sup>+1</code> is the composition of the successor function and the squaring function (first we square, then we take the successor).
+
The composition of a function `f` with itself, namely:
\x. f (f x)
And indeed this is the Church encoding of the numbers:
-<code>0 ≡ \f z. I z ; or \f z. f<sup>0</sup> z</code>
-<code>1 ≡ \f z. f z ; or \f z. f<sup>1</sup> z</code>
-<code>2 ≡ \f z. f (f z) ; or \f z. f<sup>2</sup> z</code>
-<code>3 ≡ \f z. f (f (f z)) ; or \f z. f<sup>3</sup> z</code>
+<code>0 ≡ \f z. z ; <~~> \f z. I z, or \f z. f<sup>0</sup> z</code>
+<code>1 ≡ \f z. f z ; or \f z. f<sup>1</sup> z</code>
+<code>2 ≡ \f z. f (f z) ; or \f z. f<sup>2</sup> z</code>
+<code>3 ≡ \f z. f (f (f z)) ; or \f z. f<sup>3</sup> z</code>
<code>...</code>
-The encoding for `0` is equivalent to `\f z. z`, which we've also proposed as the encoding for `[]` and for `false`. Don't read too much into this.
+The encoding for `0` is what we also proposed as the encoding for `[]` and for `false`. Don't read too much into this.
Given the above, can you figure out how to define the `succ` function? We already worked through the definition of `cons`, and this is just a simplification of that, so you should be able to do it. We'll make it a homework.