∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (c : C),
  CategoryTheory.Grothendieck.ι F c =
    { obj := fun d => { base := c, fiber := d },
      map := fun {X Y} f =>
        { base := CategoryTheory.CategoryStruct.id { base := c, fiber := X }.base,
          fiber := CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f },
      map_id := ⋯, map_comp := ⋯ }