∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C CategoryTheory.Cat}
  (α : F ⟶ F') (c : C),
  CategoryTheory.Grothendieck.ιCompMap α c =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        CategoryTheory.Iso.refl (((CategoryTheory.Grothendieck.ι F c).comp (CategoryTheory.Grothendieck.map α)).obj X))
      ⋯