∀ {C₁ : Type u_2} {C₂ : Type u_5} {C₃ : Type u_6} {C₄ : Type u_10} [inst : CategoryTheory.Category.{u_3, u_2} C₁]
  [inst_1 : CategoryTheory.Category.{u_11, u_5} C₂] [inst_2 : CategoryTheory.Category.{u_12, u_6} C₃]
  [inst_3 : CategoryTheory.Category.{u_9, u_10} C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_1}
  {I₂ : Type u_7} {I₃ : Type u_8} {J : Type u_4} (p : I₁ × I₂ × I₃ → J)
  [inst_4 :
    ∀ (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂)
      (X₃ : CategoryTheory.GradedObject I₃ C₃),
      ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
  {X Y Z : CategoryTheory.GradedObject I₁ C₁} (f : X ⟶ Y) (g : Y ⟶ Z),
  {
      app := fun X₂ =>
        {
          app := fun X₃ =>
            CategoryTheory.GradedObject.mapTrifunctorMapMap F p (CategoryTheory.CategoryStruct.comp f g)
              (CategoryTheory.CategoryStruct.id X₂) (CategoryTheory.CategoryStruct.id X₃),
          naturality := ⋯ },
      naturality := ⋯ } =
    CategoryTheory.CategoryStruct.comp
      {
        app := fun X₂ =>
          {
            app := fun X₃ =>
              CategoryTheory.GradedObject.mapTrifunctorMapMap F p f (CategoryTheory.CategoryStruct.id X₂)
                (CategoryTheory.CategoryStruct.id X₃),
            naturality := ⋯ },
        naturality := ⋯ }
      {
        app := fun X₂ =>
          {
            app := fun X₃ =>
              CategoryTheory.GradedObject.mapTrifunctorMapMap F p g (CategoryTheory.CategoryStruct.id X₂)
                (CategoryTheory.CategoryStruct.id X₃),
            naturality := ⋯ },
        naturality := ⋯ }