#Contents# * table of contents {:toc} ## 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$$ 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}$$ ## See also ## * [[differential function]] * [[Newton-Leibniz operator]]