{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} →
              {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₃} →
                    (hom : (i : ι) → D₁.obj i ⟶ D₂.obj i) →
                      autoParam
                          (∀ (i₁ i₂ : ι),
                            CategoryTheory.CategoryStruct.comp ((F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (hom i₁))
                                (D₂.hom i₁ i₂) =
                              CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂)
                                ((F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (hom i₂)))
                          CategoryTheory.Pseudofunctor.DescentData'.Hom.comm._autoParam →
                        D₁.Hom D₂