∀ {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} {S' : C} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} (e : S' ≅ S)
  {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)}
  (w :
    ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = CategoryTheory.CategoryStruct.comp (f' j) e.hom)
  {β : ι → ι'} {q' : (i : ι) → X i ⟶ X' (β i)}
  (w' :
    ∀ (i : ι), CategoryTheory.CategoryStruct.comp (q' i) (f' (β i)) = CategoryTheory.CategoryStruct.comp (f i) e.inv),
  (CategoryTheory.Pseudofunctor.DescentData.pullFunctorEquivalence F e w w').functor =
    CategoryTheory.Pseudofunctor.DescentData.pullFunctor F w