∀ {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} {D₁ D₂ : F.DescentData f} (self : D₁.Hom D₂) ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄
  (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
  (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q) {Z : ↑(F.obj { as := Opposite.op Y })}
  (h : (F.map f₂.op.toLoc).toFunctor.obj (D₂.obj i₂) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.map f₁.op.toLoc).toFunctor.map (self.hom i₁))
      (CategoryTheory.CategoryStruct.comp (D₂.hom q f₁ f₂ ⋯ ⋯) h) =
    CategoryTheory.CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯)
      (CategoryTheory.CategoryStruct.comp ((F.map f₂.op.toLoc).toFunctor.map (self.hom i₂)) h)