functor_bicategory): bicategory structure on oplax functors (#11405)

Commit

4 years ago

feat(category_theory/bicategory/functor_bicategory): bicategory structure on oplax functors (#11405) This PR defines a bicategory structure on the oplax functors between bicategories.

Author

yuma-mizuno

Parents

da164c6b

mathlib c3d87824 - feat(category_theory/bicategory/functor_bicategory): bicategory structure on oplax functors (#11405)

mathlib
c3d87824 - feat(category_theory/bicategory/functor_bicategory): bicategory structure on oplax functors (#11405)