functor): define oplax functors and their composition (#11277)

Commit

4 years ago

feat(category_theory/bicategory/functor): define oplax functors and their composition (#11277) This PR defines oplax functors between bicategories and their composition.

Author

yuma-mizuno

Parents

624cb707

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

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