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