∀ {V : Type u_4} [inst : Quiver V] {C : Type u_2} [inst_1 : CategoryTheory.Category.{u_1, u_2} C] (φ : V ⥤q C)
  {X Y Z : CategoryTheory.Paths V} (f : X ⟶ Y) (g : Y ⟶ Z),
  Quiver.Path.rec (CategoryTheory.CategoryStruct.id (φ.obj X))
      (fun {b c} x f ihp => CategoryTheory.CategoryStruct.comp ihp (φ.map f)) (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp
      (Quiver.Path.rec (CategoryTheory.CategoryStruct.id (φ.obj X))
        (fun {b c} x f ihp => CategoryTheory.CategoryStruct.comp ihp (φ.map f)) f)
      (Quiver.Path.rec (CategoryTheory.CategoryStruct.id (φ.obj Y))
        (fun {b c} x f ihp => CategoryTheory.CategoryStruct.comp ihp (φ.map f)) g)