Tính kết hợp của phép bằng từ Eq.rec

Cố định $a,b$ và $h_1 : a = b$. Cho $h_2 : b = c$ với $c$ tuỳ ý, ta muốn chứng minh $a = c$. Áp dụng $\mathsf{Eq.rec}$ lên $h_2$ với motive $C(y, h) := (a = y)$, chỉ số theo điểm $y$ và chứng minh $h$ nối $b$ với $y$.

Trường hợp gốc cần là $C(b, \mathrm{refl}\,b)$, tức $a = b$ — chính là $h_1$. Vậy $h_1$ là chứng minh trường hợp gốc cấp cho $\mathsf{Eq.rec}$.

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

Vậy $\mathrm{Eq.trans}\,h_1\,h_2 := \mathsf{Eq.rec}\,(C := \lambda y\, h,\, a = y)\,h_1\,c\,h_2$ có kiểu $\mathrm{Eq.trans} : a = b \to b = c \to a = c$. Chú ý mẫu hình chung với đối xứng: cả hai chứng minh đều "vận chuyển" một sự kiện theo một phép bằng bằng cách chọn motive $C$ phù hợp, rồi để quy tắc rút gọn cố định của hạt nhân cho $\mathsf{Eq.rec}$ trên $\mathrm{refl}$ làm việc thật.