For a calculus field?$F$ and a subtype $S \subseteq F$, the type of smooth functions or infinitely differentiable functions between $S$ and $F$ is defined as the maximal subtype $C^\infty(S, F) \subseteq S \to F$ such that the inverse image of $C^\infty(S, F)$ under the Newton-Leibniz operator is equivalent to $C^\infty(S, F)$ itself.