Sort u →
  {J : Type u_1} →
    {K : Type u_2} →
      [inst : CategoryTheory.Category.{v_1, u_1} J] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
          {C : Type u_3} →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} →
                CategoryTheory.Limits.DiagramOfCones F →
                  {J' : Type u_1} →
                    {K' : Type u_2} →
                      [inst' : CategoryTheory.Category.{v_1, u_1} J'] →
                        [inst'_1 : CategoryTheory.Category.{v_2, u_2} K'] →
                          {C' : Type u_3} →
                            [inst'_2 : CategoryTheory.Category.{v_3, u_3} C'] →
                              {F' : CategoryTheory.Functor J' (CategoryTheory.Functor K' C')} →
                                CategoryTheory.Limits.DiagramOfCones F' → Sort u