Theorems · Theorem · category theory

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

Defined in

Mathlib.Combinatorics.Quiver.Prefunctor

Cited by

5 results in Mathlib

Foundations

Depth 5 from the axioms · uses Quot.sound

Assumes

QuiverQuiver