∀ {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)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  {D₁ D₂ : F.DescentData' sq sq₃} (e : (i : ι) → D₁.obj i ≅ D₂.obj i),
  (∀ (i₁ i₂ : ι),
      CategoryTheory.CategoryStruct.comp ((F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (e i₁).hom) (D₂.hom i₁ i₂) =
        CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂) ((F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (e i₂).hom)) →
    ∀ (i₁ i₂ : ι),
      CategoryTheory.CategoryStruct.comp ((F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (e i₁).inv) (D₁.hom i₁ i₂) =
        CategoryTheory.CategoryStruct.comp (D₂.hom i₁ i₂) ((F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (e i₂).inv)