∀ {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} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S} {α : ι' → ι}
  {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = f' j)
  {D₁ D₂ : F.DescentData f}
  (φ φ_1 :
    (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₁ ⟶
      (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₂),
  φ = φ_1 →
    ∀ (i : ι) ⦃Y : CategoryTheory.Over (X i)⦄
      (f_1 f_2 : Y ⟶ CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id (X i))) (e_f : f_1 = f_2)
      (a : (CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve✝ f f' i).arrows f_1),
      CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.familyOfElements✝ w φ i f_1 a =
        CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.familyOfElements✝¹ w φ_1 i f_2 ⋯