Sort u_1 →
  {J : Type u} →
    [inst : CategoryTheory.Category.{v, u} J] →
      {F : CategoryTheory.Functor J (Type w₀)} →
        F.CoconeTypes →
          {J' : Type u} →
            [inst' : CategoryTheory.Category.{v, u} J'] →
              {F' : CategoryTheory.Functor J' (Type w₀)} → F'.CoconeTypes → Sort u_1