∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G)
  {X Y : CategoryTheory.Grothendieck F} (f : X ⟶ Y), ((CategoryTheory.Grothendieck.map α).map f).base = f.base