Def CategoryTheory.Functor.toPseudoFunctor'

Modification history

2026-02-20 18:02
Mathlib/CategoryTheory/Bicategory/Functor/LocallyDiscrete.lean
doc(CategoryTheory/Bicategory/Functor): clean up docstrings (#34978) …
Deleted CategoryTheory.Functor.toPseudoFunctor'View on Github →
2025-11-03 17:34
Mathlib/CategoryTheory/Bicategory/Functor/LocallyDiscrete.lean
chore(Pseudofunctor): add notation of pseudofunctors (#31171) …
Modified CategoryTheory.Functor.toPseudoFunctor'View on Github →
2025-06-08 16:23
Mathlib/CategoryTheory/Bicategory/Functor/LocallyDiscrete.lean
feat(Bicategory/Functor/LocallyDiscrete): add `Functor.toPseudofunctor` (#25569) …
Added CategoryTheory.Functor.toPseudoFunctor'View on Github →