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

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

# Contents

## Definition

Given a calculus field$F$sequentially Cauchy complete Archimedean ordered field and a F \mathbb{R} - and acalculus vector space?real vector space $V$, a scalar function  f:V \to F \mathbb{R} is a directionally differentiable function if for every vector $v:V$ and line $L_v \subseteq V$,

 L_v \coloneqq \sum_{v:V} \Vert \sum_{a:F} \sum_{a:\mathbb{R}} v = a w \Vert

with canonical equivalence  m:F m:\mathbb{R} \cong L_v and canonical inclusion $i:L_v \hookrightarrow V$, the composite $f \circ i \circ m$ is a differentiable function.