∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddGrpCat),
  AddGrpCat.FilteredColimits.colimitNeg F =
    { neg := fun x => Quot.lift (AddGrpCat.FilteredColimits.colimitNegAux F) ⋯ x }