Prefunctor.ext

theorem Prefunctor.ext : ∀ {V : Type u} [inst : Quiver V] {W : Type u₂} [inst_1 : Quiver W] {F G : V ⥤q W} (h_obj : ∀ (X : V), F.obj X = G.obj X), (∀ (X Y : V) (f : X ⟶ Y), F.map f = Eq.recOn ⋯ (Eq.recOn ⋯ (G.map f))) → F = G

The theorem `Prefunctor.ext` states that given two prefunctors `F` and `G` from a category `V` to a category `W`, if for every object `X` in `V` the objects `F.obj X` and `G.obj X` in `W` are equal, and for every morphism `f` from `X` to `Y` in `V`, the morphisms `F.map f` and `G.map f` in `W` are equal (up to an equality conversion specified by `Eq.recOn`), then the two prefunctors `F` and `G` are equal. This theorem provides a criterion for the equality of prefunctors in terms of their action on objects and morphisms.

More concisely: Given two prefunctors F and G from category V to category W, if for all objects X in V, F.obj X = G.obj X, and for all morphisms f: X -> Y in V, F.map f = G.map f, then F = G.