∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : C}
  (f : X ⟶ Y) (d : ↑(F.obj X)), ((CategoryTheory.Grothendieck.ιNatTrans f).app d).base = f