locally_discrete): define locally discrete bicategory (#11402)

Commit

4 years ago

feat(category_theory/bicategory/locally_discrete): define locally discrete bicategory (#11402) This PR defines the locally discrete bicategory on a category.

Author

yuma-mizuno

Parents

6dd65257

mathlib3 ff9b7574 - feat(category_theory/bicategory/locally_discrete): define locally discrete bicategory (#11402)

mathlib3
ff9b7574 - feat(category_theory/bicategory/locally_discrete): define locally discrete bicategory (#11402)