Transitivity of equality from Eq.rec

Fix $a,b$ and $h_1 : a = b$. Given $h_2 : b = c$ for arbitrary $c$, we want a proof of $a = c$. Apply $\mathsf{Eq.rec}$ to $h_2$ with motive $C(y, h) := (a = y)$, indexed by the point $y$ and the proof $h$ connecting $b$ to $y$.

The base case required is $C(b, \mathrm{refl}\,b)$, i.e. $a = b$ — exactly $h_1$. So $h_1$ is the base-case proof supplied to $\mathsf{Eq.rec}$.

$\mathsf{Eq.rec}$ then delivers, for every $c$ and every $h_2 : b = c$, a proof of $C(c, h_2) = (a = c)$, which is what we wanted.

So $\mathrm{Eq.trans}\,h_1\,h_2 := \mathsf{Eq.rec}\,(C := \lambda y\, h,\, a = y)\,h_1\,c\,h_2$ has type $\mathrm{Eq.trans} : a = b \to b = c \to a = c$. Notice the pattern shared with symmetry: both proofs "transport" a fact along an equality by choosing the right motive $C$, then let the kernel's fixed reduction rule for $\mathsf{Eq.rec}$ on $\mathrm{refl}$ do the actual work.