从Eq.rec推出相等的对称性

固定 $a$。我们想要一个函数,对任意 $b$,把 $h : a = b$ 变成 $b = a$ 的证明。用动机(motive)$C(y, h) := (y = a)$ 来使用 $\mathsf{Eq.rec}$——这是一族由点 $y$ 及连接 $a$ 到 $y$ 的证明 $h$ 索引的命题。

消去子要求提供基础情形 $C(a, \mathrm{refl}\,a)$ 的证明,即 $a = a$;我们提供 $\mathrm{refl}\,a$ 本身。这是合法的,因为基础情形总是在起点 $a$ 处由 $\mathrm{refl}$ 索引。

于是 $\mathsf{Eq.rec}$ 对每个 $y$ 与每个 $h : a = y$ 返回 $C(y,h) = (y = a)$ 的证明。代入 $y := b,\ h := h$:我们恰好得到 $b = a$ 的证明。

把它打包为 $\mathrm{Eq.symm}\,h := \mathsf{Eq.rec}\,(C := \lambda y\, h,\, y = a)\,(\mathrm{refl}\,a)\,b\,h$,就得到类型为 $\mathrm{Eq.symm} : a = b \to b = a$ 的项。内核仅通过将这个应用与 $\mathsf{Eq.rec}$ 的类型签名匹配就能接受它——在内核层面完全不需要对"对称性"这一概念进行推理。