∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C}
  {X : ι → C} (f : (i : ι) → X i ⟶ S),
  F.IsPrestackFor (CategoryTheory.Presieve.ofArrows X f) ↔ Nonempty (F.toDescentData f).FullyFaithful