∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))} {I₁ : Type u_7}
  {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {p : I₁ × I₂ × I₃ → J} {X₁ : CategoryTheory.GradedObject I₁ C₁}
  {X₂ : CategoryTheory.GradedObject I₂ C₂} {X₃ : CategoryTheory.GradedObject I₃ C₃} {Y : C₄} {j : J}
  [inst_4 : ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
  {φ φ' : CategoryTheory.GradedObject.mapTrifunctorMapObj F p X₁ X₂ X₃ j ⟶ Y},
  φ = φ' ↔
    ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : p (i₁, i₂, i₃) = j),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
          φ =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
          φ'