# Homotopy Type Theory difference quotient > history (Rev #4, changes)

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

# Contents

## Definition

Given a Heyting field $F$ and a subtype $S \subseteq F$, let us define the subtype $\Delta_{\#}(S) \subseteq S \times S$ of pairs of elements apart from the diagonal as

$\Delta_{\#}(S) \coloneqq \sum_{(x,y):S \times S} x \# y$

### In a field

Given a function $f:S \to F$, the difference quotient $q:\Delta_{\#}(S) \to F$ is the partial binary function

$q(x, y) := \frac{f(x) - f(y)}{x - y}$

### In a vector space

Given a $F$-bimodule $V$ and a function $f:S \to V$, the difference quotient $q:\Delta_{\#}(S) \to V$ is the partial binary function

$q(x, y) := \frac{1}{x - y} (f(x) - f(y))$