∀ {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} {S' : C} {p : S' ⟶ S} {ι' : Type u_6} {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)
  (D : F.DescentData f) (Y : C) (q : Y ⟶ S') (j₁ j₂ j₃ : ι') (f₁ : Y ⟶ X' j₁) (f₂ : Y ⟶ X' j₂) (f₃ : Y ⟶ X' j₃)
  (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f' j₁) = q) (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f' j₂) = q)
  (hf₃ : CategoryTheory.CategoryStruct.comp f₃ (f' j₃) = q),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom w D (CategoryTheory.CategoryStruct.comp f₁ (f' j₁)) f₁
        f₂ ⋯ ⋯)
      (CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom w D (CategoryTheory.CategoryStruct.comp f₂ (f' j₂)) f₂
        f₃ ⋯ ⋯) =
    CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom w D (CategoryTheory.CategoryStruct.comp f₁ (f' j₁)) f₁ f₃
      ⋯ ⋯