English
A refined extensionality principle for reflexive prefunctors equates equality to a simple endomorphism-preserving condition.
Русский
Уточненная экстенсивная формула для рефлексивных префункторов устанавливает равенство при простом условии сохранения структуры на концах.
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_X).symm (h_Y).symm$$$
Lean4
/-- This may be a more useful form of `ReflPrefunctor.ext`. -/
theorem ext' {V W : Type u} [ReflQuiver.{v} V] [ReflQuiver.{v} W] {F G : ReflPrefunctor 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 ⟨Fpre, Fid⟩ := F
obtain ⟨Gpre, Gid⟩ := G
obtain rfl : Fpre = Gpre := Prefunctor.ext' (V := V) (W := W) h_obj h_map
rfl
