-> Nat)` as the second argument for `hfoldB `. Such function would need to be defined for any type `b`, so it cannot be useful for defining the summation. (4) Unlike the induction principle for list, it is not clear how to obtain an induction principle for `Bush` from the higher-order fold `hfoldB`.

As a result, in the pioneer works of *generalized folds* for nested data types by Bird and Paterson ([@bird1999generalised], [@bird1999bruijn]), they have to define generalized folds using maps, and both generalized folds and map functions are defined by general recursion. As for the formal verification, nested data types such as `Bush` can not be declared directly in the dependently typed language Coq[^2]. In Agda, although we can declare nested data types such as `Bush`, we cannot easily program and reason about higher-order folds. This is because: (1) The Agda termination checker fails to recognize the termination of higher-order folds defined from general recursion. (2) Currently there is no natural formulation of induction principles for nested data types similar to the ones for regular data types.

Contributions of the paper
--------------------------

We present an approach to define fold functions for nested data types using dependent types inside the 