∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_5, u_3} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type u_1} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentData f} (e : (i : ι) → D₁.obj i ≅ D₂.obj i)
  (comm :
    ∀ ⦃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),
      CategoryTheory.CategoryStruct.comp ((F.map f₁.op.toLoc).toFunctor.map (e i₁).hom) (D₂.hom q f₁ f₂ ⋯ ⋯) =
        CategoryTheory.CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯) ((F.map f₂.op.toLoc).toFunctor.map (e i₂).hom)),
  CategoryTheory.CategoryStruct.comp { hom := fun i => (e i).inv, comm := ⋯ } { hom := fun i => (e i).hom, comm := ⋯ } =
    CategoryTheory.CategoryStruct.id D₂