Theorems · Theorem · category theory

CategoryTheory.Quiv.freeMap_pathsOf_pathComposition

∀ (V : Type u) [inst : Quiver V],
  (CategoryTheory.Cat.freeMap (CategoryTheory.Paths.of V)).comp
      (CategoryTheory.pathComposition (CategoryTheory.Paths V)) =
    CategoryTheory.Functor.id (CategoryTheory.Paths V)

Defined in

Mathlib.CategoryTheory.Category.Quiv

Cited by

0 results in Mathlib

Foundations

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

Assumes

Quiver