Characterization of (pre)stacks for a precoverage

Let F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat be a pseudofunctor. Assuming F is a prestack for a Grothendieck topology J, we show that if f : X i ⟶ S and f' : X' j ⟶ S are two covering families of morphisms in S such that the sieve generated by f' is contained in the sieve generated by f, then the functor F.DescentData f ⥤ F.DescentData f' is full.

TODO (@joelriou): show that the functor is also faithful, and deduce characterizations of (pre)stacks.

theorem CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {J : GrothendieckTopology C} [F.IsPrestack J] {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S} {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryStruct.comp (p' j) (f (α j)) = f' j) (hf' : Sieve.ofArrows X' f' ∈ J S) : (pullFunctor F ⋯).Full