Structure CategoryTheory.Oplax.OplaxTrans

Modification history

2025-11-05 18:48
Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Oplax.lean
chore(Bicategory/Functor): add notation for lax and oplax functors (#31238) …
Modified CategoryTheory.Oplax.OplaxTransView on Github →
2025-04-25 04:02
Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Oplax.lean
feat(Bicategory/Oplax): Fix simp lemmas and renaming (#18252) …
Added CategoryTheory.Oplax.OplaxTransView on Github →