Def CategoryTheory.Functor.toPseudoFunctor

Modification history

2025-06-08 16:23
Mathlib/CategoryTheory/Bicategory/Functor/LocallyDiscrete.lean
feat(Bicategory/Functor/LocallyDiscrete): add `Functor.toPseudofunctor` (#25569) …
Modified CategoryTheory.Functor.toPseudoFunctorView on Github →
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.toPseudoFunctorView on Github →
2024-05-17 19:31
Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean
style: remove all isolated `where` (#12991)
Modified CategoryTheory.Functor.toPseudoFunctorView on Github →
2024-04-25 15:18
Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean
feat(CategoryTheory/Bicategory/LocallyDiscrete): Make LocallyDiscrete a structure (#12383) …
Added CategoryTheory.Functor.toPseudoFunctorView on Github →