Commit 2025-11-05 18:48 4fbef235

View on Github →

chore(Bicategory/Functor): add notation for lax and oplax functors (#31238) I am open to suggestion for other notation as well.

Estimated changes

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

modified structure CategoryTheory.LaxFunctor.PseudoCore

modified def CategoryTheory.LaxFunctor.comp

modified def CategoryTheory.LaxFunctor.id

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

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

modified structure CategoryTheory.OplaxFunctor.PseudoCore

modified def CategoryTheory.OplaxFunctor.comp

modified def CategoryTheory.OplaxFunctor.id

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

modified def CategoryTheory.Pseudofunctor.mkOfLax

modified def CategoryTheory.Pseudofunctor.mkOfOplax

modified def CategoryTheory.Pseudofunctor.toLax

modified def CategoryTheory.Pseudofunctor.toOplax

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

modified structure CategoryTheory.StrictlyUnitaryLaxFunctor

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

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

modified theorem CategoryTheory.Oplax.OplaxTrans.Modification.comp_app'

modified theorem CategoryTheory.Oplax.OplaxTrans.Modification.id_app'

modified theorem CategoryTheory.Oplax.OplaxTrans.ext

Modified Mathlib/CategoryTheory/Bicategory/Monad/Basic.lean

modified def CategoryTheory.Bicategory.Comonad.ofOplaxFromUnit

modified def CategoryTheory.Bicategory.Comonad.toOplax

modified def CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.toOplax

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

modified structure CategoryTheory.Oplax.OplaxTrans.StrongCore

modified structure CategoryTheory.Oplax.OplaxTrans

modified def CategoryTheory.Oplax.StrongTrans.mkOfOplax

modified def CategoryTheory.Oplax.StrongTrans.toOplax

modified structure CategoryTheory.Oplax.StrongTrans

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