{J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      (F : CategoryTheory.Functor J AddGrpCat) → (j : J) × ↑(F.obj j) → ↑(AddGrpCat.FilteredColimits.G F)