Commit 2024-07-20 11:58 f26425b2

promoting the Grothendieck construction into a functor (#14387) This PR adds the functoriality of the Grothendieck construction by providing

map (α : F ⟶ G) : Grothendieck F ⥤ Grothendieck G

and then promotes the Grothendieck construction into a functor from the functor category C ⥤ Cat to the over category Over C in the category of categories:

def functor {E : Cat.{v,u}} : (E ⥤ Cat.{v,u}) ⥤ Over (T:= Cat.{v,u}) E