∀ {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} {p : S' ⟶ 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)) = CategoryTheory.CategoryStruct.comp (f' j) p)
  {β : ι' → ι} {p'' : (j : ι') → X' j ⟶ X (β j)}
  (w' : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p'' j) (f (β j)) = CategoryTheory.CategoryStruct.comp (f' j) p)
  (X_1 : F.DescentData f) (i : ι'),
  ((CategoryTheory.Pseudofunctor.DescentData.pullFunctorIso F w w').hom.app X_1).hom i =
    X_1.hom (CategoryTheory.CategoryStruct.comp (p' i) (f (α i))) (p' i) (p'' i) ⋯ ⋯