Sort u_1 →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {J : Type w} →
        [inst_1 : CategoryTheory.Category.{t, w} J] →
          {X : C} →
            CategoryTheory.Limits.LimitPresentation J X →
              {C' : Type u} →
                [inst' : CategoryTheory.Category.{v, u} C'] →
                  {J' : Type w} →
                    [inst'_1 : CategoryTheory.Category.{t, w} J'] →
                      {X' : C'} → CategoryTheory.Limits.LimitPresentation J' X' → Sort u_1