Theorems · Theorem · category theory

CategoryTheory.Cat.freeReflMap_map

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

Defined in

Mathlib.CategoryTheory.Category.ReflQuiv

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.ReflQuiverCategoryTheory.ReflQuiver