## Exercise 3.17

The universal property for foldN is presumably:

    h = foldN z s

    iff

    h n = case n of
            Zero   → z
            Succ m → s (h m)

for all h : Nat → α.  I’d like to know how we can prove that this
is indeed a universal property.

To derive a fusion law, we need a solution to the equation:

    f ∘ foldN z s = foldN z' s'

Using the above universal property, we know that this holds iff:

    (f ∘ foldN z s) Zero     = z'
    (f ∘ foldN z s) (Succ n) = s' ((f ∘ foldN z s) n)

The solution to the first equation is almost immediate:

      z' = f (foldN z s Zero)

    ≡   { foldN.1 }

      z' = f z

For the second equation, we reason as follows:

      s' (f (foldN z s n)) = f (foldN z s (Succ n))

    ≡   { foldN.2 }

      s' (f (foldN z s n)) = f (s (foldN z s n))

    ≡   { generalizing (foldN z s n) to x }

      s' (f x) = f (s x)

    ≡   { rewrite as a composition, η-equivalence }

      s' ∘ f = f ∘ s

which gives a constraint for s'.

So we have the following fusion law:

    f ∘ foldN z s = foldN z' s'

    if

    (f z = z') ∧ (s' ∘ f = f ∘ s)