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