There is a nice lemma on adjoint functors, purely 2-categorical, and certainly known to various colleagues. As I need it in a paper on homotopy, I would like to know if it is *published with proof*, somewhere. I also like to "advertise" it here, because I think it deserves to be known more widely. LEMMA. If,in an adjunction, any one of the four natural transformations which appear in the triangle identities is invertible, so are the other three. [Proof below.] A few years ago I was considering such adjunctions, which I was calling "connections" because adjunctions between ordered sets ("covariant Galois connections") are always of this type. Renato Betti was also considering them, under the name of "exact adjunctions" (which I now prefer, also because "connection" has already too many meanings). I learnt from him that "one condition is sufficient". At my knowledge, the above result appears in two works. It is cited without proof in - R.Betti, Adjointness in descent theory, JPAA 116 (1997), 41-47. It also appears, with a proof and in a more general formulation (for biadjoints), in a preprint: - R.Betti, D. Schumacher and R. Street, Factorizations in bicategories, Dip. Mat. Politecnico di Milano n. 22/R, 1999. ___ Proof. Write F -| G the adjunction; u: 1 -> GF the unit; v: FG -> 1 the counit. The triangle identities say that (a) vF.Fu = idF, (b) Gv.uG = idG. Assume that Fu is invertible, so that also vF is so and it is sufficient to prove that: (c) uG.Gv = id(GFG). This commposite occurs in the upper row of the following commutative diagram (vertical arrows down) Gv uG GFG ----> G ----> GFG uGFG | |uG |uGFG GFGFG ----> GFG ----> GFGFG GFGv GFuG Now, the lower row is the identity, because G(Fu)G is invertible and the "other composite", GF(Gv.uG) is an identity, by (b). Since the vertical arrow uGFG has a left inverse, by (b) again, "cancelling it from the outer rectangle" we get (c). [Perhaps it can be simplified; I did not spent much time for that.] ___