∀ {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