Commit 2023-03-13 13:46 baf8d765

View on Github →

feat: port CategoryTheory.Bicategory.LocallyDiscrete (#2813)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean

added def CategoryTheory.Functor.toOplaxFunctor

added theorem CategoryTheory.LocallyDiscrete.eq_of_hom

added def CategoryTheory.LocallyDiscrete