Symmetry of equality from Eq.rec

Fix $a$. We want a function taking $h : a = b$ (for arbitrary $b$) to a proof of $b = a$. Apply $\mathsf{Eq.rec}$ with the motive $C(y, h) := (y = a)$ — a family of propositions indexed by the point $y$ and the proof $h$ connecting $a$ to $y$.

The eliminator asks for a proof of the base case $C(a, \mathrm{refl}\,a)$, i.e. of $a = a$; supply $\mathrm{refl}\,a$ itself. This is legal because the base case is always indexed by $\mathrm{refl}$ at the starting point $a$.

$\mathsf{Eq.rec}$ then returns, for every $y$ and every $h : a = y$, a proof of $C(y,h) = (y = a)$. Instantiate $y := b,\ h := h$: we obtain exactly a proof of $b = a$.

Packaging this as $\mathrm{Eq.symm}\,h := \mathsf{Eq.rec}\,(C := \lambda y\, h,\, y = a)\,(\mathrm{refl}\,a)\,b\,h$ gives the term of type $\mathrm{Eq.symm} : a = b \to b = a$. The kernel accepts it purely by matching this application against the type signature of $\mathsf{Eq.rec}$ — no reasoning about "symmetry" as a concept is needed at the kernel level.