∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {X Y : CategoryTheory.Grothendieck F} (h : X = Y), (CategoryTheory.eqToHom h).fiber = CategoryTheory.eqToHom ⋯