Commit 2026-02-20 18:02 cf0ed141

View on Github →

doc(CategoryTheory/Bicategory/Functor): clean up docstrings (#34978) Fix doc-only inconsistencies across bicategory functor files.

Estimated changes

Modified Mathlib/CategoryTheory/Bicategory/Functor/Cat/ObjectProperty.lean

Modified Mathlib/CategoryTheory/Bicategory/Functor/Lax.lean

Modified Mathlib/CategoryTheory/Bicategory/Functor/LocallyDiscrete.lean

deleted def CategoryTheory.Functor.toPseudoFunctor'

deleted def CategoryTheory.Functor.toPseudoFunctor

added def CategoryTheory.Functor.toPseudofunctor'

added def CategoryTheory.Functor.toPseudofunctor

Modified Mathlib/CategoryTheory/Bicategory/Functor/Oplax.lean

Modified Mathlib/CategoryTheory/Bicategory/Functor/Prelax.lean

Modified Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean

Modified Mathlib/CategoryTheory/Bicategory/Functor/StrictPseudofunctor.lean

Modified Mathlib/CategoryTheory/Bicategory/Functor/StrictlyUnitary.lean