Lean4
/-- The Grothendieck construction is functorial: a natural transformation `α : F ⟶ G` induces
a functor `Grothendieck.map : Grothendieck F ⥤ Grothendieck G`.
-/
@[simps!]
def map (α : F ⟶ G) : Grothendieck F ⥤ Grothendieck G
where
obj
X :=
{ base := X.base
fiber := (α.app X.base).obj X.fiber }
map {X Y}
f :=
{ base := f.base
fiber := (eqToHom (α.naturality f.base).symm).app X.fiber ≫ (α.app Y.base).map f.fiber }
map_id X := by simp only [Cat.eqToHom_app, id_fiber, eqToHom_map, eqToHom_trans]; rfl
map_comp {X Y Z} f
g := by
dsimp
congr 1
simp only [← Category.assoc, Functor.map_comp, eqToHom_map]
congr 1
simp only [Cat.eqToHom_app, Cat.comp_obj, eqToHom_trans, eqToHom_map, Category.assoc, ← Cat.comp_map]
rw [Functor.congr_hom (α.naturality g.base).symm f.fiber]
simp
