{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {A : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
          {motive : CategoryTheory.HasSheafify J A → Sort u} →
            ((isRightAdjoint : CategoryTheory.HasWeakSheafify J A) →
                (isLeftExact :
                    CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.sheafToPresheaf J A).leftAdjoint) →
                  motive ⋯) →
              (t : CategoryTheory.HasSheafify J A) → motive t