Eq.recからの等号の対称性

$a$ を固定する。任意の $b$ について $h : a = b$ を受け取り $b = a$ の証明を返す関数が欲しい。モチーフ $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}$ の型シグネチャと照合するだけで受理し、「対称性」という概念について推論する必要はカーネルの水準では一切ない。