Commit 2025-12-01 19:09 2310ec31

View on Github →

feat(Bicategory/FunctorBicategory): add type aliases for 2-morphisms in functor bicategories (#32301)

Estimated changes

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

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

added structure CategoryTheory.Oplax.OplaxTrans.Hom

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

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

modified theorem CategoryTheory.Oplax.OplaxTrans.homCategory.ext

added structure CategoryTheory.Oplax.StrongTrans.Hom

modified theorem CategoryTheory.Oplax.StrongTrans.homCategory.ext

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

added structure CategoryTheory.Pseudofunctor.StrongTrans.Hom

modified theorem CategoryTheory.Pseudofunctor.StrongTrans.homCategory.ext