feat(category_theory/bicategory/functor): define oplax functors and their composition (#11277)
feat(category_theory/bicategory/functor): define oplax functors and their composition (#11277)

This PR defines oplax functors between bicategories and their composition.





leanprover-community/mathlib,leanprover-community/mathlib