∀ {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)