mathlib

371b48a0 - feal(category_theory/bicategory/functor): define pseudofunctors (#11992)

feal(category_theory/bicategory/functor): define pseudofunctors (#11992) This PR defines pseudofunctors between bicategories. We provide two constructors (`mk_of_oplax` and `mk_of_oplax'`) that construct pseudofunctors from oplax functors whose `map_id` and `map_comp` are isomorphisms. The constructor `mk_of_oplax` uses `iso` to describe isomorphisms, while `mk_of_oplax'` uses `is_iso`. Co-authored-by: Scott Morrison <scott@tqft.net>