 Natural-number fold

For data Natural = Zero | Succ Natural, replace Zero by a base value and Succ by a step function: foldNat g a Zero = a and foldNat g a (Succ n) = g (foldNat g a n). On a finite total natural number $n$ this iterates $g$ exactly $n$ times.