# Homotopy Type Theory differentiable function > history (Rev #6, changes)

Showing changes from revision #5 to #6: Added | Removed | Changed

# Contents

## Definition

### Valued in fields

Given an Archimedean ordered field $F$, a pointwise continuous function $f:F \to F$ is pointwise differentiable if it comes with a function $D(f):F \to F$ called the derivative and such that for every positive element $\epsilon:F_+$, there exists a positive element $\delta:F_+$ such that for every element $h:F$ such that $0 \lt \max(h, -h) \lt \delta$ and for every element $x:F$,

Given a algebraic limit field $F$, a subtype $S \subseteq F$, a pointwise continuous function $f:C^0(S, F)$ is differentiable if the difference quotient has a limit approaching the diagonal

$\vert f(x + h) - f(x) - h D(f)(x) \vert \lt \epsilon$
$isDifferentiable(f) := hasLimitApproachingDiagonal\left(\frac{f(x) - f(y)}{x - y}\right)$

Let us define the type of differentiable functions $D^1(S, F)$ on $S$ as the type of pointwise continuous functions that are differentiable.

$D^1(S, F) := \sum_{f:C^0(S, F)} isDifferentiable(f)$