English
Equality of reflexive prefunctors follows from equality of their underlying prefunctor structure and a compatible map formula.
Русский
Равенство рефлексивного префункторa следует из равенства базовой структуры и совместной формулы отображения.
LaTeX
$$$\\text{Ext on ReflPrefunctor: } F=G \\text{ if } F.obj=G.obj \\text{ and } F.map=G.map$$$
Lean4
/-- Proving equality between reflexive prefunctors. This isn't an extensionality lemma,
because usually you don't really want to do this. -/
theorem ext {V : Type u} [ReflQuiver.{v₁} V] {W : Type u₂} [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 = 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 := (Set.eqOn_univ F_obj G_obj).mp fun _ _ ↦ h_obj _
congr
funext X Y f
simpa using h_map X Y f
