English
Let f: X → Y and g: Z → Z' be morphisms in a category, and h be an equality Y = W. Then the heterogeneous equality f ≍ g is unchanged if we replace Y by W on the left side by composing f with the canonical map provided by h; i.e. f ≫ eqToHom h is HEq to g exactly when f is HEq to g.
Русский
Пусть f: X → Y и g: Z → Z' — морфизмы в category, и h — равенство Y = W. Тогда неоднородное равенство f ≍ g сохраняется при замене Y на W слева посредством композиции с каноническим отображением, заданным равенством h; то есть f ≫ eqToHom h ≍ g тогда и только тогда, когда f ≍ g.
LaTeX
$$$ f \\circ eqToHom(h) \\; \\mathrel{\\equiv} \\; g \\; \\Longleftrightarrow \\; f \\mathrel{\\equiv} g $$$
Lean4
@[simp]
theorem comp_eqToHom_heq_iff {C} [Category C] {W X Y Z Z' : C} (f : X ⟶ Y) (g : Z ⟶ Z') (h : Y = W) :
f ≫ eqToHom h ≍ g ↔ f ≍ g :=
⟨(comp_eqToHom_heq ..).symm.trans, (comp_eqToHom_heq ..).trans⟩
