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}$ に対するカーネルの固定された還元規則に委ねている。