∀ {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}
  (hP : CategoryTheory.Presheaf.IsSheaf J P) (S : J.Cover X) (x : (I : S.Arrow) → E ⟶ P.obj (Opposite.op I.Y))
  (hx :
    ∀ ⦃I₁ I₂ : S.Arrow⦄ (r : I₁.Relation I₂),
      CategoryTheory.CategoryStruct.comp (x I₁) (P.map r.g₁.op) =
        CategoryTheory.CategoryStruct.comp (x I₂) (P.map r.g₂.op))
  (I : S.Arrow) {Z : A} (h : P.obj (Opposite.op I.Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (hP.amalgamate S x hx) (CategoryTheory.CategoryStruct.comp (P.map I.f.op) h) =
    CategoryTheory.CategoryStruct.comp (x I) h