∀ {C : Type u_1} [inst : CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : PresheafOfModules R),
  CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair M.fromFreeYonedaCoproduct 0)