English
Prefunctors commute with transporting arrows along equality of endpoints: F.map (homOfEq f hX hY) equals homOfEq (F.map f) with endpoints transported.
Русский
Префункторы commute с переносом стрел по равенствам концов: отображение F.map (homOfEq f hX hY) равно homOfEq (F.map f) с переносами концов.
LaTeX
$$$F.map (Quiver.homOfEq f hX hY) = Quiver.homOfEq (F.map f) (congr\\_arg F.obj hX) (congr\\_arg F.obj hY)$$$
Lean4
/-- Prefunctors commute with `homOfEq`. -/
@[simp]
theorem homOfEq_map {U V : Type*} [Quiver U] [Quiver V] (F : U ⥤q V) {X Y : U} (f : X ⟶ Y) {X' Y' : U} (hX : X = X')
(hY : Y = Y') :
F.map (Quiver.homOfEq f hX hY) = Quiver.homOfEq (F.map f) (congr_arg F.obj hX) (congr_arg F.obj hY) := by
subst hX hY; simp
