Theorems · Theorem · category theory

CategoryTheory.Cat.FreeRefl.functor_ext

∀ {V : Type u_1} [inst : CategoryTheory.ReflQuiver V] {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} D]
  {F G : CategoryTheory.Functor (CategoryTheory.Cat.FreeRefl V) D}
  (h₁ : ∀ (v : V), F.obj (CategoryTheory.Cat.FreeRefl.mk v) = G.obj (CategoryTheory.Cat.FreeRefl.mk v)),
  (∀ {v w : V} (f : v ⟶ w),
      F.map (CategoryTheory.Cat.FreeRefl.homMk f) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
          (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Cat.FreeRefl.homMk f))
            (CategoryTheory.eqToHom ⋯))) →
    F = G

Defined in

Mathlib.CategoryTheory.Category.ReflQuiv

Cited by

1 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.ReflQuiverCategoryTheory.Category