∀ {C₁ : Type u_8} {C₂ : Type u_10} {C₃ : Type u_2} {C₄ : Type u_5} [inst : CategoryTheory.Category.{u_7, u_8} C₁]
  [inst_1 : CategoryTheory.Category.{u_9, u_10} C₂] [inst_2 : CategoryTheory.Category.{u_6, u_2} C₃]
  [inst_3 : CategoryTheory.Category.{u_4, u_5} C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_11}
  {I₂ : Type u_12} {I₃ : Type u_3} {J : Type u_1} (p : I₁ × I₂ × I₃ → J) (X₁ : CategoryTheory.GradedObject I₁ C₁)
  [inst_4 :
    ∀ (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₂ : CategoryTheory.GradedObject I₂ C₂),
  {
      app := fun X₃ =>
        CategoryTheory.GradedObject.mapTrifunctorMapMap F p (CategoryTheory.CategoryStruct.id X₁)
          (CategoryTheory.CategoryStruct.id X₂) (CategoryTheory.CategoryStruct.id X₃),
      naturality := ⋯ } =
    CategoryTheory.CategoryStruct.id
      { obj := fun X₃ => CategoryTheory.GradedObject.mapTrifunctorMapObj F p X₁ X₂ X₃,
        map := fun {x x_1} φ =>
          CategoryTheory.GradedObject.mapTrifunctorMapMap F p (CategoryTheory.CategoryStruct.id X₁)
            (CategoryTheory.CategoryStruct.id X₂) φ,
        map_id := ⋯, map_comp := ⋯ }