∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5}
  [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₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} {ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r}
  {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂}
  {X₃ : CategoryTheory.GradedObject I₃ C₃}
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
              (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
          X₃).HasMap
      ρ₁₂.q]
  [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] {j : J} {A : C₄}
  {f g :
    CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q
        (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j ⟶
      A},
  f = g ↔
    ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) f =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) g