∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u_6}
  [inst_1 : CategoryTheory.Category.{u_5, u_6} J] (F : CategoryTheory.Functor J (PresheafOfModules R))
  [inst_2 :
    ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
      CategoryTheory.Limits.PreservesColimit (F.comp (PresheafOfModules.evaluation R Y))
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))]
  [inst_3 : ∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))] {X Y : J}
  (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (F.map f)
      { app := fun X => CategoryTheory.Limits.colimit.ι (F.comp (PresheafOfModules.evaluation R X)) Y,
        naturality := ⋯ } =
    CategoryTheory.CategoryStruct.comp
      { app := fun X_1 => CategoryTheory.Limits.colimit.ι (F.comp (PresheafOfModules.evaluation R X_1)) X,
        naturality := ⋯ }
      (((CategoryTheory.Functor.const J).obj (PresheafOfModules.colimitPresheafOfModules F)).map f)