$\gdef\spaces#1{~ #1 ~}$
$\gdef\R{\mathbf{R}}$
首先需要强调的是, 这个公理所涉及到的结构的有效性全都依赖于 意象理论, 而相关基础的严格性保证基本上在 1970 年之前就已经由 William Lawvere 完工. 记 $\mathcal{E}$ 是光滑空间之间的光滑映射构成的范畴, 同时假定 $\mathcal{E}$ 还是笛卡尔闭范畴, 也就是 $\mathcal{E}$ 中的箭头对笛卡尔积封闭.
我们可以从 $\mathcal{E}$ 中选出一条几何直线 $R$, 通过指定 $R$ 上两点 $0$ 和 $1$ 之间的距离作为单位长度来确定其他线段的长度. 发挥一些古希腊精神, 线段的移动可以给出 $R$ 上的加法, 尺规作图所构造的 相似三角形 能给出 $R$ 上的乘法 $\gamma = \alpha\beta$.
Methods in Algebra - Volume 1, p. 369
因此 $R$ 带有交换环结构, 并且允许经典数学中的对象实数环 $\R$ 成为 $R$ 的模型, 注意这里我们只能考虑 $\R$ 作为环的部分, 因为 $R$ 中存在着幂零元.
Kock–Lawvere 公理说的是, 对任意映射 $f: D \to R$, 存在唯一的 $a,b \in R$, 使得
$$
f(\epsilon) \spaces= a + b \epsilon, \quad \forall \epsilon \in D
$$
将这里的 $a$ 换成 $f(0)$, 并完全使用量词叙述, 则是
$$
\forall ~ f \in R^D, ~ \exists! ~ b ~ \text{s.t.} ~ \forall ~ d \in D \quad (f(d) = f(0) + b d)
$$
如果说这个公理的形式还不足以暗示它的目的, 那么下面这个推论就完全能做到了.
$\gdef\quads#1{\quad #1 \quad}$
$\gdef\spaces#1{~ #1 ~}$
对任意函数 $f:R \rightarrow R$, 存在唯一的函数 $f':R \rightarrow R$ 满足
$$
f(x + \varepsilon) \spaces= f(x) + f'(x)\varepsilon,\quad \forall ~ x \in R, ~ \forall ~ \varepsilon \in D
$$
这个通常作为 Kock–Lawvere 公理 的推论出现, 不过从 $\mathcal{E}$ 的定义来看, 这才是整套框架真正的目的之一. 即, 为全体函数恢复牛顿时期 “幂零无穷小量” 计算上的直观, 而不导致矛盾.