{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 F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))} →
                  (F ≅ F') →
                    (I₁ : Type u_7) →
                      (I₂ : Type u_8) →
                        (I₃ : Type u_9) →
                          CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃ ≅
                            CategoryTheory.GradedObject.mapTrifunctor F' I₁ I₂ I₃