{J₁ : Type u_1} →
  {J₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] →
        {C₁ : Type u_3} →
          {C₂ : Type u_4} →
            {C : Type u_5} →
              [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] →
                    (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C)) →
                      {K₁ : CategoryTheory.Functor J₁ C₁} →
                        {K₂ : CategoryTheory.Functor J₂ C₂} →
                          CategoryTheory.Limits.Cocone K₁ →
                            CategoryTheory.Limits.Cocone K₂ →
                              CategoryTheory.Limits.Cocone
                                (CategoryTheory.Functor.uncurry.obj
                                  ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))