English
A refined extensionality: equality of Prefunctors can be witnessed by equality of object parts and a compatible map formula using homOfEq.
Русский
Уточненная экстенсивность: равенство префункторов можно доказать равенством частей объектов и подходящей формулой отображения через homOfEq.
LaTeX
$$$F=G$ whenever\\forall X, F.obj X = G.obj X\\;\\land\\;\\forall X Y f, F.map f = Quiver.homOfEq (G.map f) (h\\_obj Y).symm (h\\obj X).symm$$$
Lean4
/-- This may be a more useful form of `Prefunctor.ext`. -/
theorem ext' {V W : Type u} [Quiver V] [Quiver 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 = Quiver.homOfEq (G.map f) (h_obj _).symm (h_obj _).symm) : F = G :=
by
obtain ⟨Fobj, Fmap⟩ := F
obtain ⟨Gobj, Gmap⟩ := G
obtain rfl : Fobj = Gobj := funext h_obj
simp only [mk.injEq, heq_eq_eq, true_and]
ext X Y f
simpa only [Quiver.homOfEq_rfl] using h_map X Y f
