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