Commit 2020-09-11 13:30 842a3246
View on Github →feat(category_theory): the Grothendieck construction (#3896)
Given a functor F : C ⥤ Cat,
the objects of grothendieck F consist of dependent pairs (b, f), where b : C and f : F.obj c,
and a morphism (b, f) ⟶ (b', f') is a pair β : b ⟶ b' in C, and φ : (F.map β).obj f ⟶ f'.
(This is only a special case of the real thing: we should treat Cat as a 2-category and allow F to be a 2-functor / pseudofunctor.)