{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {motive : CategoryTheory.GrothendieckTopology C → Sort u_1} →
      ((sieves : (X : C) → Set (CategoryTheory.Sieve X)) →
          (top_mem' : ∀ (X : C), ⊤ ∈ sieves X) →
            (pullback_stable' :
                ∀ ⦃X Y : C⦄ ⦃S : CategoryTheory.Sieve X⦄ (f : Y ⟶ X),
                  S ∈ sieves X → CategoryTheory.Sieve.pullback f S ∈ sieves Y) →
              (transitive' :
                  ∀ ⦃X : C⦄ ⦃S : CategoryTheory.Sieve X⦄,
                    S ∈ sieves X →
                      ∀ (R : CategoryTheory.Sieve X),
                        (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → CategoryTheory.Sieve.pullback f R ∈ sieves Y) →
                          R ∈ sieves X) →
                motive
                  { sieves := sieves, top_mem' := top_mem', pullback_stable' := pullback_stable',
                    transitive' := transitive' }) →
        (t : CategoryTheory.GrothendieckTopology C) → motive t