∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat}
  {inst_1 : ∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)}
  {inst_2 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat}
  {inst_3 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat} {M : SheafOfModules R} {I : Type w} {X : I → C}
  {coversTop : J.CoversTop X} {presentation : (i : I) → (M.over (X i)).Presentation} {I_1 : Type w} {X_1 : I_1 → C}
  {coversTop_1 : J.CoversTop X_1} {presentation_1 : (i : I_1) → (M.over (X_1 i)).Presentation},
  { I := I, X := X, coversTop := coversTop, presentation := presentation } =
      { I := I_1, X := X_1, coversTop := coversTop_1, presentation := presentation_1 } →
    I = I_1 ∧ X ≍ X_1 ∧ presentation ≍ presentation_1