∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat),
  CategoryTheory.Pseudofunctor.CoGrothendieck.map (CategoryTheory.CategoryStruct.id F) =
    CategoryTheory.Functor.id F.CoGrothendieck