∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommMonCat)
  [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections],
  Small.{u, max u v}
    ↑((F.comp (CategoryTheory.forget₂ AddCommMonCat AddMonCat)).comp (CategoryTheory.forget AddMonCat)).sections