{J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      (F : CategoryTheory.Functor J AddCommMonCat) → AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M F)