∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C CategoryTheory.Cat}
  (α : F ⟶ F') (c : C) (X : ↑(F.obj c)),
  ((CategoryTheory.Grothendieck.ιCompMap α c).inv.app X).fiber = CategoryTheory.eqToHom ⋯