Many times, we encounter that two adjunctions do not compose because they are the wrong way around. In many of these cases, we can observe that the unit of the second is invertible. Somehow, this means we can still compose the adjunctions! This can be proved in formal category theory using string diagrams for bicategories.
This version of the lemma appeared in Collages of String Diagrams (Braithwaite, Román, 2023).
