Commit 2022-01-19 06:53 ff9b7574

View on Github →

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

Estimated changes

Created src/category_theory/bicategory/locally_discrete.lean

added def category_theory.functor.to_oplax_functor

added def category_theory.locally_discrete

Modified src/category_theory/bicategory/strict.lean

added theorem category_theory.bicategory.eq_to_hom_whisker_right

added theorem category_theory.bicategory.whisker_left_eq_to_hom