step) xs))

The fold function `hfoldB` for the nested data type `Bush` is called a *higher-order fold* in the literature (e.g. [@bird1999generalised], [@johann2007initial]). Observe that the type variable `p` in `hfoldB` is generalized to kind `Set -> Set`. The higher-order fold `hfoldB` has the following problems. (1) The definition of `hfoldB` requires the map function `hmapB`, and `hmapB` can not be defined from `hfoldB`. (2) For both `hmapB` and `hfoldB`, Agda’s termination checker fails because the use of recursion in both cases are not well-founded. For example, in the second case of `hmapB`, the outer recursive call of `hmapB` is on the structurally smaller argument `xs`, but there is no such indication for the inner recursive call `(hmapB f)`. (3) Although possible (see Section \[related\]), it is not immediately clear how `hfoldB` can be used to define functions such as a summation of all the entries in `Bush Nat`. The most obvious way is to instantiate `p` with ` x -> Nat` for `hfoldB`, thus `hfoldB ` has type `( -> Nat) -> ( -> b -> Nat -> Nat) -> Bush Nat -> Nat`. We will have to provide a function of the type `( -> b -> Nat 