Def CategoryTheory.Bicategory.Adj.Bicategory.leftUnitor

Modification history

2025-06-25 10:15

Mathlib/CategoryTheory/Bicategory/Adjunction/Adj.lean

feat: the bicategory of adjunctions in a bicategory (#25977) …

Added CategoryTheory.Bicategory.Adj.Bicategory.leftUnitor View on Github →