∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type u_5} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} (sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j))
  (D : F.DescentData f) (i : ι),
  CategoryTheory.Pseudofunctor.DescentData'.pullHom' (fun i₁ i₂ => D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯)
      (f i) (CategoryTheory.CategoryStruct.id (X i)) (CategoryTheory.CategoryStruct.id (X i)) ⋯ ⋯ =
    CategoryTheory.CategoryStruct.id ((F.map (CategoryTheory.CategoryStruct.id (X i)).op.toLoc).toFunctor.obj (D.obj i))