to the higher-order folds. In Section \[related\], we discuss related work. In Section \[final\], we discuss future work and conclude the paper. All the detailed programs for each section are available at <https://github.com/Fermat/dependent-fold> and checked by Agda 2.5.3.

A development of dependently typed folds in a total type theory via the Bush data type {#dev}
======================================================================================

Let us continue the consideration of the `Bush` data type. The following is the result of evaluating `hmapB f bush1`, where `f : Nat -> b` for some type `b`.

      [ f 4,                                            -- b
        [ f 8, [ f 5 ], [ [ f 3 ] ] ],             -- Bush b
        [ [ f 7 ], [ ], [ [ [ f 7 ] ] ] ],  -- Bush (Bush b)
        [ [ [ ], [ [ f 0 ] ] ] ]     -- Bush (Bush (Bush b))
      ]                -- Bush (Bush (Bush (Bush (Bush b))))

In order to define the map function for `Bush Nat`, we need to already have the map functions defined for $\texttt{Bush}^n \ \texttt{Nat}$ for all $n \geq 0$, which seems paradoxical. A way out is to define a general map function for $\texttt{Bush}^n$, for all $n \geq 