∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat),
  PresheafOfModules.toPresheaf R =
    { obj := fun M => M.presheaf,
      map := fun {X Y} f =>
        { app := fun X_1 => AddCommGrpCat.ofHom (AddMonoidHom.mk' ⇑(CategoryTheory.ConcreteCategory.hom (f.app X_1)) ⋯),
          naturality := ⋯ },
      map_id := ⋯, map_comp := ⋯ }