Theorems · Theorem · category theory

CategoryTheory.Cat.FreeRefl.lift_map

∀ {V : Type u_1} [inst : CategoryTheory.ReflQuiver V] {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} D]
  (F : V ⥤rq D) {v w : V} (f : v ⟶ w),
  (CategoryTheory.Cat.FreeRefl.lift F).map (CategoryTheory.Cat.FreeRefl.homMk f) = F.map f

Defined in

Mathlib.CategoryTheory.Category.ReflQuiv

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.ReflQuiverCategoryTheory.Category