∀ {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} (M : ↑(F.obj { as := Opposite.op S })) (i : ι),
  (CategoryTheory.Pseudofunctor.DescentData.ofObj M).obj i = (F.map (f i).op.toLoc).toFunctor.obj M