{C : Type u_1} →
  [inst : CategoryTheory.SmallCategory C] →
    [CategoryTheory.IsFiltered C] →
      (R : CategoryTheory.Functor C RingCat) →
        (M : CategoryTheory.Functor C Ab) →
          [inst_2 : (i : C) → Module ↑(R.obj i) ↑(M.obj i)] →
            (∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
                (CategoryTheory.ConcreteCategory.hom (M.map f)) (r • m) =
                  (CategoryTheory.ConcreteCategory.hom (R.map f)) r •
                    (CategoryTheory.ConcreteCategory.hom (M.map f)) m) →
              {cR : CategoryTheory.Limits.Cocone R} →
                CategoryTheory.Limits.IsColimit cR →
                  {cM : CategoryTheory.Limits.Cocone M} → CategoryTheory.Limits.IsColimit cM → Module ↑cR.pt ↑cM.pt