Theorem CategoryTheory.Oplax.OplaxTrans.homCategory.ext

Modification history

2025-12-01 19:09
Mathlib/CategoryTheory/Bicategory/Modification/Oplax.lean
feat(Bicategory/FunctorBicategory): add type aliases for 2-morphisms in functor bicategories (#32301)
Modified CategoryTheory.Oplax.OplaxTrans.homCategory.extView on Github →
2025-11-28 10:31
Mathlib/CategoryTheory/Bicategory/Modification/Oplax.lean
feat(Bicategory/Modification/Pseudo): define modifications between strong natural transformations of pseudofunctors (#30895) …
Added CategoryTheory.Oplax.OplaxTrans.homCategory.extView on Github →