0$. First we define $\texttt{Bush}^n$ as the following `NBush`.

    NTimes : (Set -> Set) -> Nat -> Set -> Set
    NTimes p Z s = s
    NTimes p (S n) s = p (NTimes p n s)
    NBush : Nat -> Set -> Set
    NBush = NTimes Bush

The function `NTimes` is a type level function defined by pattern-matching on the natural number `n`. The function call `NTimes p n a` returns a type of the form $\texttt{p}^n\ a$. We now define the following map function `mapB` for $\texttt{Bush}^n$, where `mapB (S Z)` corresponds to the map function for `Bush a`.

    mapB : {a b : Set} -> (n : Nat) -> (a -> b) -> NBush n a -> NBush n b 
    mapB Z f x = f x
    mapB (S n) f NilB = NilB
    mapB (S n) f (ConsB x xs) = ConsB (mapB n f x) (mapB (S (S n)) f xs) 

The recursive definition of `mapB` is well-founded as all the recursive calls are on the components of the constructor `ConsB`. The Agda termination checker accepts this definition of `mapB`. The definition of `mapB` confirms a general principle in theorem proving: proving a more general 