Theorem CategoryTheory.Oplax.OplaxTrans.ext

Modification history

2025-11-28 10:31
Mathlib/CategoryTheory/Bicategory/Modification/Oplax.lean
feat(Bicategory/Modification/Pseudo): define modifications between strong natural transformations of pseudofunctors (#30895) …
Deleted CategoryTheory.Oplax.OplaxTrans.extView on Github →
2025-11-05 18:48
Mathlib/CategoryTheory/Bicategory/Modification/Oplax.lean
chore(Bicategory/Functor): add notation for lax and oplax functors (#31238) …
Modified CategoryTheory.Oplax.OplaxTrans.extView on Github →
2025-05-12 14:24
Mathlib/CategoryTheory/Bicategory/Modification/Oplax.lean
feat(Bicategory/NaturalTransformation): strong transformations between pseudofunctors (#18253) …
Added CategoryTheory.Oplax.OplaxTrans.extView on Github →