Theorems · Theorem · category theory

CategoryTheory.FreeBicategory.inclusionPathAux.eq_def

∀ {B : Type u} [inst : Quiver B] {a : B} (x : B) (x_1 : Quiver.Path a x),
  CategoryTheory.FreeBicategory.inclusionPathAux x_1 =
    match x, x_1 with
    | .(a), Quiver.Path.nil => CategoryTheory.FreeBicategory.Hom.id a
    | x, p.cons f => (CategoryTheory.FreeBicategory.inclusionPathAux p).comp (CategoryTheory.FreeBicategory.Hom.of f)

Defined in

Mathlib.CategoryTheory.Bicategory.Coherence

Cited by

0 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

Quiver