{J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J RingCat) →
      [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget RingCat)).sections] →
        CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ RingCat SemiRingCat)