# Homotopy Type Theory smooth function > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

# Contents

## Definition

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.

$p: (C^\infty(S, F) \subseteq S \to F) \times \left(C^\infty(S, F) \cong \sum_{f:D^1(S, F)} \Vert\sum_{g:C^\infty(S, F)} \tilde{D}(f) = g\Vert\right)$
$p: \prod_{T:\mathcal{U}} (T \subseteq S \to F) \times \left(T \cong \sum_{f:D^1(S, F)} \Vert\sum_{g:T} \tilde{D}(f) = g\Vert\right) \to (T \subseteq C^\infty(S, F))$