basic): define bicategories (#11079)

Commit

4 years ago

feat(category_theory/bicategory/basic): define bicategories (#11079) This PR defines bicategories and gives basic lemmas.

Author

yuma-mizuno

Parents