  A well-known problem in the theory of dependent types is how to handle
so-called nested data types. These data types are difficult to program and to
reason about in total dependently typed languages such as Agda and Coq. In
particular, it is not easy to derive a canonical induction principle for such
types. Working towards a solution to this problem, we introduce dependently
typed folds for nested data types. Using the nested data type Bush as a guiding
example, we show how to derive its dependently typed fold and induction
principle. We also discuss the relationship between dependently typed folds and
the more traditional higher-order folds.
