∀ {𝒮 : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 𝒮]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (S : 𝒮)
  (a : ↑(F.obj { as := Opposite.op S })), ((CategoryTheory.Pseudofunctor.CoGrothendieck.ι F S).obj a).base = S