Def CategoryTheory.OplaxNatTrans.leftUnitor

Modification history

2025-05-12 14:24

Mathlib/CategoryTheory/Bicategory/FunctorBicategory/Oplax.lean

feat(Bicategory/NaturalTransformation): strong transformations between pseudofunctors (#18253) …

Deleted CategoryTheory.OplaxNatTrans.leftUnitor View on Github →

2023-06-12 05:44

Mathlib/CategoryTheory/Bicategory/FunctorBicategory.lean

feat: port CategoryTheory.Bicategory.FunctorBicategory (#4976)

Added CategoryTheory.OplaxNatTrans.leftUnitor View on Github →