Theorems · Theorem · category theory

CategoryTheory.Paths.ext_functor

∀ {V : Type u₁} [inst : Quiver V] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  {F G : CategoryTheory.Functor (CategoryTheory.Paths V) C} (h_obj : F.obj = G.obj),
  (∀ (a b : V) (e : a ⟶ b),
      F.map e.toPath =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
          (CategoryTheory.CategoryStruct.comp (G.map e.toPath) (CategoryTheory.eqToHom ⋯))) →
    F = G

Two functors out of a path category are equal when they agree on singleton paths.

Defined in

Mathlib.CategoryTheory.PathCategory.Basic

Cited by

6 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext, Quot.sound

Assumes

QuiverCategoryTheory.Category