Commit 2025-06-25 10:15 ab494ff4

feat: the bicategory of adjunctions in a bicategory (#25977) Given a bicategory B, we construct a bicategory Adj B that has the same objects but whose 1-morphisms are adjunctions (in the same direction as the left adjoints), and 2-morphisms are tuples of mate maps between the left and right adjoints (where the map between right adjoints is in the opposite direction).