Commit 2025-06-08 16:23 a4ec7db3

feat(Bicategory/Functor/LocallyDiscrete): add Functor.toPseudofunctor (#25569) We add Functor.toPseudofunctor which takes a functor between categories and returns the corresponding pseudofunctor between locally discrete categories. Previously, Functor.toPseudofunctor took a functor from a category to a strict bicategory, and returned the corresponding pseudofunctor. Since this new construction works for all functors, I suggest that this takes the name Functor.toPseudofunctor and the latter gets renamed to Functor.toPseudofunctor'.