feat(CategoryTheory/Bicategory/Grothendieck): functors between Grothendieck constructions induced by strong natural transforms

[robin-carlier]

Generalize the content of CategoryTheory/Grothendieck to pseudofunctor and show that a strong oplax natural transformation of pseudofunctors induces a functor between the Grothendieck contsructions, and that the construction preserves composition and identities.

---

The proof of map_comp_eq is rather slow and needs a slight increase in heartbeats to go through. It’s probably golfable.