∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {K : CategoryTheory.GrothendieckTopology D} {G : CategoryTheory.Functor C D},
  (∀ (ℱ : CategoryTheory.Sheaf K (Type w)) {Z : C} {T : CategoryTheory.Presieve Z}
      {x : CategoryTheory.Presieve.FamilyOfElements (G.op.comp ℱ.val) T},
      x.Compatible →
        ∀ {Y₁ Y₂ : C} {X : D} (f₁ : X ⟶ G.obj Y₁) (f₂ : X ⟶ G.obj Y₂) {g₁ : Y₁ ⟶ Z} {g₂ : Y₂ ⟶ Z} (hg₁ : T g₁)
          (hg₂ : T g₂),
          CategoryTheory.CategoryStruct.comp f₁ (G.map g₁) = CategoryTheory.CategoryStruct.comp f₂ (G.map g₂) →
            ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)) →
    CategoryTheory.CompatiblePreserving K G