Def CategoryTheory.LocallyDiscrete.mkPseudofunctor

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) …

Added CategoryTheory.LocallyDiscrete.mkPseudofunctor View on Github →