∀ {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} (X_1 : F.DescentData f) (i : ι),
  ((CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso F S).hom.app X_1).hom i =
    (F.mapId { as := Opposite.op (X i) }).hom.toNatTrans.app (X_1.obj i)