lengthB {a} = foldB {a} {\ n -> Nat} (\ x -> Z) (\ n -> Z) (\ n r1 r2 -> S r2) (S Z)

Comparing the dependently typed fold `foldB` and the higher-order fold `hfoldB` in Section \[intro\], we can see that `foldB` does not depend on map, and `mapB` can be defined from `foldB`. The termination of `foldB` is obvious and it can be used to define other terminating functions. Moreover, the higher-order fold `hfoldB` is an instance of the dependently typed fold `foldB`, as we can define `hfoldB` using `foldB`.

    hfoldB : {a : Set} -> {p : Set -> Set} -> 
              ({b : Set} -> p b) -> ({b : Set} -> b -> p (p b) -> p b) -> Bush a -> p a
    hfoldB {a} {p} base step = 
      foldB {a} {\ n -> NTimes p n a} (\ x -> x) (\ n -> base) (\ n -> step) (S Z)

Last but not least, we can generalize the type of dependently typed fold `foldB` to obtain the following induction principle `indB`, just like how we obtain the induction principle for `List` from its fold function.

    indB : {a : Set} 