∀ {J : Type u_2} [inst : CategoryTheory.Category.{u_3, u_2} J] (F : CategoryTheory.Functor J SemiRingCat),
  1 ∈ (MonCat.sectionsSubmonoid (F.comp (CategoryTheory.forget₂ SemiRingCat MonCat))).carrier