{C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_4} →
      {C₂₃ : Type u_5} →
        {E : Type u_9} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃] →
                [inst_3 : CategoryTheory.Category.{v_5, u_5} C₂₃] →
                  [inst_4 : CategoryTheory.Category.{v_9, u_9} E] →
                    (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ E)) →
                      (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) →
                        CategoryTheory.bifunctorComp₂₃ F G₂₃ ≅
                          CategoryTheory.Functor.curry.obj
                            (CategoryTheory.Functor.curry.obj
                              ((CategoryTheory.prod.associator C₁ C₂ C₃).comp
                                (CategoryTheory.Functor.uncurry.obj
                                  ((CategoryTheory.Functor.uncurry.obj G₂₃).comp F.flip).flip)))