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