English
Let X, X′, Y, Y′ be objects of a quiver, with f: X → Y and g: X′ → Y′, and with identifications hX: X′ = X and hY: Y′ = Y. Then f equals the transported arrow HomOfEq g along hX,hY if and only if HomOfEq f along the inverses equals g.
Русский
Пусть X, X′, Y, Y′ — объекты кьювера, f: X → Y и g: X′ → Y′, и существуют тождества hX: X′ = X, hY: Y′ = Y. Тогда f = перенесённая стрелка g через hX,hY тогда и только если перенесенная обратно стрелка f через обратные тождества равна g.
LaTeX
$$$ f = \\operatorname{homOfEq}(g,hX,hY) \\iff \\operatorname{homOfEq}(f,hX^{-1},hY^{-1}) = g $$$
Lean4
theorem eq_homOfEq_iff {X X' Y Y' : V} (f : X ⟶ Y) (g : X' ⟶ Y') (hX : X' = X) (hY : Y' = Y) :
f = Quiver.homOfEq g hX hY ↔ Quiver.homOfEq f hX.symm hY.symm = g := by subst hX hY; simp
