∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (α : F ⟶ G),
  (CategoryTheory.Pseudofunctor.CoGrothendieck.map α).comp (CategoryTheory.Pseudofunctor.CoGrothendieck.forget G) =
    CategoryTheory.Pseudofunctor.CoGrothendieck.forget F