Def CategoryTheory.OplaxNatTrans.rightUnitor

Modification history

2023-06-12 05:44

Mathlib/CategoryTheory/Bicategory/FunctorBicategory.lean

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

Added CategoryTheory.OplaxNatTrans.rightUnitor View on Github →