English
For Path objects p from u to v and p' from u' to v', with hu: u = u' and hv: v = v', the equality p.cast hu hv = p' is equivalent to p and p' being heterogeneously equal.
Русский
Для путей p: u → v и p': u' → v', при hu: u = u' и hv: v = v', равенство p.cast hu hv = p' эквивалентно тому, что p и p' относятся к друг другу как неоднородно равные.
LaTeX
$$$ p' = p^{cast}_{hu hv} \\iff p \\;\\stackrel{HEQ}{\\sim}\\; p' $$$
Lean4
theorem eq_cast_iff_heq {u v u' v' : U} (hu : u = u') (hv : v = v') (e : u ⟶ v) (e' : u' ⟶ v') :
e' = e.cast hu hv ↔ e' ≍ e := by
rw [eq_comm, Hom.cast_eq_iff_heq]
exact ⟨HEq.symm, HEq.symm⟩