{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F :
        CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
          (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              {D₁ D₂ : F.DescentDataAsCoalgebra f} →
                {motive : D₁.Hom D₂ → Sort u_1} →
                  (t : D₁.Hom D₂) →
                    ((hom : (i : ι) → D₁.obj i ⟶ D₂.obj i) →
                        (comm :
                            ∀ (i₁ i₂ : ι),
                              CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂)
                                  ((F.map (f i₁).op.toLoc).l.toFunctor.map
                                    ((F.map (f i₂).op.toLoc).r.toFunctor.map (hom i₂))) =
                                CategoryTheory.CategoryStruct.comp (hom i₁) (D₂.hom i₁ i₂)) →
                          motive { hom := hom, comm := comm }) →
                      motive t