# Homotopy Type Theory iterated differentiable 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 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:

$D^0(S, F) := \tilde{D}^{-0}(S \to F) := S \to F$
$n:\mathbb{N} \vdash D^{n+1}(S, F) := \tilde{D}^{-(n+1)}(S \to F) := \sum_{f:D^1(S, F)} \Vert\sum_{g:D^{n}(S, F)} \tilde{D}(f) = g\Vert$

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:

$C^0(S, F) := \tilde{D}^{-0}(C^0(S, F)) := C^0(S, F)$
$n:\mathbb{N} \vdash C^{n+1}(S, F) := \tilde{D}^{-(n+1)}(C^0(S, F)) := \sum_{f:D^1(S, F)} \Vert\sum_{g:C^{n}(S, F)} \tilde{D}(f) = g\Vert$