{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} →
            {motive : CategoryTheory.CompatiblePreserving K G → Sort u} →
              (t : CategoryTheory.CompatiblePreserving K G) →
                ((compatible :
                      ∀ (ℱ : 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₂)) →
                    motive ⋯) →
                  motive t