English
Let f, g be objects of a β-indexed family of objects in C, with a morphism z_b: f(b) → g(b) for each b, and j = j'. Then z_j composed with the canonical map to the same index equals the canonical map composed with z_j'. This expresses naturality of eqToHom along a reindexing.
Русский
Пусть имеется β-индексированная семья объектов в C; z_b: f(b) → g(b) для каждого b; при j = j' выполняется природность, что z_j слева с eqToHom равно eqToHom слева на j' с z_j'.
LaTeX
$$$ z_j \\circ eqToHom(\\text{by simp [w]}) = eqToHom(\\text{by simp [w]}) \\circ z_{j'} $$$
Lean4
/-- We can push `eqToHom` to the left through families of morphisms. -/
@[reassoc (attr := simp)]
theorem eqToHom_naturality {f g : β → C} (z : ∀ b, f b ⟶ g b) {j j' : β} (w : j = j') :
z j ≫ eqToHom (by simp [w]) = eqToHom (by simp [w]) ≫ z j' :=
by
cases w
simp
