∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat]
  [inst_3 : J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {C' : Type u₂}
  [inst_4 : CategoryTheory.Category.{v₂, u₂} C'] {J' : CategoryTheory.GrothendieckTopology C'}
  {S : CategoryTheory.Sheaf J' RingCat} [inst_5 : CategoryTheory.HasSheafify J' AddCommGrpCat]
  [inst_6 : J'.WEqualsLocallyBijective AddCommGrpCat]
  [inst_7 : J'.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
  (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S))
  (η η_1 : F.obj (SheafOfModules.unit R) ≅ SheafOfModules.unit S),
  η = η_1 →
    ∀ (I : Type u) [inst_8 : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete I) F],
      SheafOfModules.mapFree F η I = SheafOfModules.mapFree F η_1 I