For a calculus field?$F$ and a subtype $S \subseteq F$, the types of functions $S \to F$, pointwise continuous functions $C^0(S, F)$, and differentiable functions $D^1(S, F)$ between $S$ and $F$ are subtypes of the type of functions $S \to F$. For the Newton-Leibniz operator$\tilde{D}: D^1(S, F) \to (S \to F)$, the type of $n$-fold iterated differentiable functions between $S$ and $F$ is the $n$-fold iterated inverse image of $S \to F$ under the Newton-Leibniz operator:

and the type of pointwise continuously $n$-fold iterated differentiable functions between $S$ and $F$ is the $n$-fold iterated inverse images of $C^0(S, F)$ under the Newton-Leibniz operator: