∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] {E : A} {X : C} {P : CategoryTheory.Functor Cᵒᵖ A},
  CategoryTheory.Presheaf.IsSheaf J P →
    ∀ (S : J.Cover X) (e₁ e₂ : E ⟶ P.obj (Opposite.op X)),
      (∀ (I : S.Arrow),
          CategoryTheory.CategoryStruct.comp e₁ (P.map I.f.op) = CategoryTheory.CategoryStruct.comp e₂ (P.map I.f.op)) →
        e₁ = e₂