∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (α : F ⟶ G),
  CategoryTheory.Pseudofunctor.CoGrothendieck.map α =
    { obj := fun a => { base := a.base, fiber := (α.app { as := Opposite.op a.base }).toFunctor.obj a.fiber },
      map := fun {a b} f =>
        { base := f.base,
          fiber :=
            CategoryTheory.CategoryStruct.comp ((α.app { as := Opposite.op a.base }).toFunctor.map f.fiber)
              ((α.naturality f.base.op.toLoc).hom.toNatTrans.app b.fiber) },
      map_id := ⋯, map_comp := ⋯ }