Adjunctions in bicategories

Mathlib's CategoryTheory.Bicategory.Adjunction is the canonical notion of an adjunction between 1-morphisms. It owns the unit, counit, triangle identities, adjoint equivalences, composition, and transport by pseudofunctors.