Theorems · Theorem · category theory

CategoryTheory.Cat.FreeRefl.lift_obj

∀ {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 : V), (CategoryTheory.Cat.FreeRefl.lift F).obj (CategoryTheory.Cat.FreeRefl.mk v) = F.obj v

Defined in

Mathlib.CategoryTheory.Category.ReflQuiv

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.ReflQuiverCategoryTheory.Category