reducing an adjunction
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.
I wrote this version of the lemma for Collages of String Diagrams (Braithwaite, Román, 2023).
