English
Two Prefunctors are equal if their object components agree and their maps agree after transporting along those equalities.
Русский
Два префункторa равны, если их объектные части совпадают и отображения согласованы после переносов по этим равенствам.
LaTeX
$$$(\\forall X, F.obj X = G.obj X)\\land(\\forall X Y f, F.map f = G.map f) \\Rightarrow F=G.$$$
Lean4
@[ext (iff := false)]
theorem ext {V : Type u} [Quiver.{v₁} V] {W : Type u₂} [Quiver.{v₂} W] {F G : Prefunctor V W}
(h_obj : ∀ X, F.obj X = G.obj X)
(h_map : ∀ (X Y : V) (f : X ⟶ Y), F.map f = Eq.recOn (h_obj Y).symm (Eq.recOn (h_obj X).symm (G.map f))) : F = G :=
by
obtain ⟨F_obj, _⟩ := F
obtain ⟨G_obj, _⟩ := G
obtain rfl : F_obj = G_obj := by
ext X
apply h_obj
congr
funext X Y f
simpa using h_map X Y f
