Tính đối xứng của phép bằng từ Eq.rec

Cố định $a$. Ta muốn một hàm nhận $h : a = b$ (với $b$ tuỳ ý) và trả về chứng minh $b = a$. Áp dụng $\mathsf{Eq.rec}$ với motive $C(y, h) := (y = a)$ — một họ mệnh đề chỉ số theo điểm $y$ và chứng minh $h$ nối $a$ với $y$.

Phép khử yêu cầu một chứng minh cho trường hợp gốc $C(a, \mathrm{refl}\,a)$, tức $a = a$; ta cấp $\mathrm{refl}\,a$. Điều này hợp lệ vì trường hợp gốc luôn được chỉ số bởi $\mathrm{refl}$ tại điểm khởi đầu $a$.

$\mathsf{Eq.rec}$ sau đó trả, với mọi $y$ và mọi $h : a = y$, một chứng minh của $C(y,h) = (y = a)$. Thay $y := b,\ h := h$: ta nhận đúng chứng minh của $b = a$.

Gói lại thành $\mathrm{Eq.symm}\,h := \mathsf{Eq.rec}\,(C := \lambda y\, h,\, y = a)\,(\mathrm{refl}\,a)\,b\,h$ cho ra hạng thức kiểu $\mathrm{Eq.symm} : a = b \to b = a$. Hạt nhân chấp nhận nó chỉ bằng cách khớp phép áp dụng này với chữ ký kiểu của $\mathsf{Eq.rec}$ — không cần lập luận về khái niệm "đối xứng" ở mức hạt nhân.