∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCat)
  [inst_1 : CategoryTheory.IsFiltered J],
  AddMonCat.FilteredColimits.colimitCocone F =
    { pt := AddMonCat.FilteredColimits.colimit F,
      ι := { app := AddMonCat.FilteredColimits.coconeMorphism F, naturality := ⋯ } }