∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat)
  [CategoryTheory.Limits.HasColimitsOfSize.{v₂, u₂, v, v + 1} AddCommGrpCat],
  CategoryTheory.Limits.HasColimitsOfSize.{v₂, u₂, max u₁ v, max (max (max (v + 1) u) u₁) v₁} (PresheafOfModules R)