{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      {J : CategoryTheory.GrothendieckTopology C} →
        {motive : F.IsStack J → Sort u_1} →
          ([toIsPrestack : F.IsPrestack J] →
              (essSurj_of_sieve : ∀ {S : C}, ∀ R ∈ J S, (F.toDescentData fun f => f.obj.hom).EssSurj) → motive ⋯) →
            (t : F.IsStack J) → motive t