∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (J : Type u_4)
  [inst_1 : CategoryTheory.Category.{u_3, u_4} J] {X Y : CategoryTheory.Arrow (CategoryTheory.Functor J C)} (τ : X ⟶ Y)
  (j : J),
  (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left τ) Y.hom).app j =
    (CategoryTheory.CategoryStruct.comp X.hom (CategoryTheory.Arrow.Hom.right τ)).app j