Def CategoryTheory.Functor.toOplaxFunctor
Modification history
2024-10-25 15:10
Mathlib/CategoryTheory/Bicategory/Functor/LocallyDiscrete.lean
feat(CategoryTheory): constructor for pseudofunctors from a strict locally discrete category (#18201) …
Modified CategoryTheory.Functor.toOplaxFunctorView on Github →