Commit 2023-08-19 02:44 2afbd9d8

feat(CategoryTheory/Bicategory): define adjunctions (#6406) This RP introduces adjunctions and adjoint equivalences in bicategories, and shows that a (non-adjoint) equivalence can be promoted to an adjoint equivalence by upgrading the counit. The constructor of adjoint equivalences only requires the left triangle identities since I will plan to show that it implies the right triangle identities in a separate PR.