∀ {C₁ : Type u_11} {C₂ : Type u_1} {C₃ : Type u_2} {C₄ : Type u_7} [inst : CategoryTheory.Category.{u_10, u_11} C₁]
  [inst_1 : CategoryTheory.Category.{u_8, u_1} C₂] [inst_2 : CategoryTheory.Category.{u_9, u_2} C₃]
  [inst_3 : CategoryTheory.Category.{u_6, u_7} C₄]
  {F F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))} (α : F ⟶ F')
  (I₁ : Type u_3) (I₂ : Type u_4) (I₃ : Type u_5) {X₁ Y₁ : CategoryTheory.GradedObject I₁ C₁} (φ : X₁ ⟶ Y₁),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).map φ)
      { app := fun X₂ => { app := fun x x_1 => ((α.app (Y₁ x_1.1)).app (X₂ x_1.2.1)).app (x x_1.2.2), naturality := ⋯ },
        naturality := ⋯ } =
    CategoryTheory.CategoryStruct.comp
      { app := fun X₂ => { app := fun x x_1 => ((α.app (X₁ x_1.1)).app (X₂ x_1.2.1)).app (x x_1.2.2), naturality := ⋯ },
        naturality := ⋯ }
      ((CategoryTheory.GradedObject.mapTrifunctor F' I₁ I₂ I₃).map φ)