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.)
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
