Theorems · Theorem · category theory

CategoryTheory.Cat.freeMap_map

∀ {V : Type u_1} {W : Type u_2} [inst : Quiver V] [inst_1 : Quiver W] (F : V ⥤q W) {X Y : CategoryTheory.Paths V}
  (a : Quiver.Path X Y), (CategoryTheory.Cat.freeMap F).map a = F.mapPath a

Defined in

Mathlib.CategoryTheory.Category.Quiv

Cited by

0 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext

Assumes

QuiverQuiver