total dependently typed language Agda. We call such folds *dependently typed folds*. Dependently typed folds are defined by well-founded recursion, hence their termination is confirmed by Agda. Map functions and many other terminating functions can be defined directly from the dependently typed folds. Moreover, the higher-order folds (such as `hfoldB`) are definable from the dependently typed folds. From the definitions of dependently typed folds, we can also obtain the corresponding induction principles. Thus we can formally reason about the programs involving nested data types in a total dependently typed language. In this paper, we illustrate these ideas by focusing on several concrete examples, we also show how to obtain dependently typed folds in general. The main technical contents of the paper are the following: In Section \[dev\], using the `Bush` data type, we develop the first example of dependently typed folds. In Section \[term\] and Section \[terme\], as a case study, we show how to define, program and reason about dependently typed folds in Agda using two well-known nested data types from the literature. In Section \[arbitrary\], we give an example to show how to obtain dependently typed folds in general, and we show how to specialize dependently typed folds 