Theorems · Theorem · category theory

CategoryTheory.composePath.eq_def

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (x : C) (x_1 : Quiver.Path X x),
  CategoryTheory.composePath x_1 =
    match x, x_1 with
    | .(X), Quiver.Path.nil => CategoryTheory.CategoryStruct.id X
    | x, p.cons e => CategoryTheory.CategoryStruct.comp (CategoryTheory.composePath p) e

Defined in

Mathlib.CategoryTheory.PathCategory.Basic

Cited by

0 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

CategoryTheory.Category