Theorems · Theorem · category theory

CategoryTheory.Cat.freeReflMap_naturality

∀ {V : Type u_3} {W : Type u_4} [inst : CategoryTheory.ReflQuiver V] [inst_1 : CategoryTheory.ReflQuiver W]
  (F : V ⥤rq W),
  (CategoryTheory.Cat.FreeRefl.quotientFunctor V).comp (CategoryTheory.Cat.freeReflMap F) =
    (CategoryTheory.Cat.freeMap F.toPrefunctor).comp (CategoryTheory.Cat.FreeRefl.quotientFunctor W)

Defined in

Mathlib.CategoryTheory.Category.ReflQuiv

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.ReflQuiverCategoryTheory.ReflQuiver