从Eq.rec推出相等的传递性

固定 $a,b$ 及 $h_1 : a = b$。给定任意 $c$ 上的 $h_2 : b = c$,我们想要 $a = c$ 的证明。用动机 $C(y, h) := (a = y)$(由点 $y$ 及连接 $b$ 到 $y$ 的证明 $h$ 索引)对 $h_2$ 使用 $\mathsf{Eq.rec}$。

所需的基础情形是 $C(b, \mathrm{refl}\,b)$,即 $a = b$——恰好就是 $h_1$。所以 $h_1$ 就是提供给 $\mathsf{Eq.rec}$ 的基础情形证明。

于是 $\mathsf{Eq.rec}$ 对每个 $c$ 与每个 $h_2 : b = c$ 给出 $C(c, h_2) = (a = c)$ 的证明,这正是我们想要的。

所以 $\mathrm{Eq.trans}\,h_1\,h_2 := \mathsf{Eq.rec}\,(C := \lambda y\, h,\, a = y)\,h_1\,c\,h_2$ 的类型是 $\mathrm{Eq.trans} : a = b \to b = c \to a = c$。注意它与对称性共享的模式:两个证明都是通过选取合适的动机 $C$,沿着一个相等关系"传输"一个事实,而真正的计算工作则交给内核对 $\mathrm{refl}$ 上 $\mathsf{Eq.rec}$ 的固定归约规则来完成。