Def CategoryTheory.OplaxNatTrans.leftUnitor

Modification history

2023-06-12 05:44

Mathlib/CategoryTheory/Bicategory/FunctorBicategory.lean

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

Added CategoryTheory.OplaxNatTrans.leftUnitor View on Github →