  We present an approach to develop folds for nested data types using dependent
types. We call such folds $\textit{dependently typed folds}$, they have the
following properties. (1) Dependently typed folds are defined by well-founded
recursion and they can be defined in a total dependently typed language. (2)
Dependently typed folds do not depend on maps, map functions and many
terminating functions can be defined using dependently typed folds. (3) The
induction principles for nested data types follow from the definitions of
dependently typed folds and the programs defined by dependently typed folds can
be formally verified. (4) Dependently typed folds exist for any nested data
types and they can be specialized to the traditional $\textit{higher-order
folds}$. Using various of examples, we show how to program and reason about
dependently typed folds. We also show how to obtain dependently typed folds in
general and how to specialize them to the corresponding higher-order folds.
