In this discussion of adjoint cylinders, I haven't noticed anyone pointing out that when L --| F --| R, then FL = Id (I use = for natural equivalence here) iff FR = Id. Dusko told me earlier this year that it was in his thesis, but I would not be surprised if it were older than that. Here is a simple proof. Let eta: Id --> FL be the inner adjunction of L --| F and epsilon: FR --> Id be the outer adjunction of F --| R. Then if alpha F means apply F,the composites alpha F Hom(eta-,F-) Hom(L-,-) -------> Hom(FL-,F-) ------------> Hom(-,F-) alpha F Hom(F-,epsilon-) Hom(-,R-) -------> Hom(F-,FR-) ----------------> Hom(F-,-) are isomorphisms. Then there is a commutative square (both composites are Hom(eta-,epsilon -) o alpha F): Hom(eta-,FR-) o alpha F Hom(L-,R-) ------------------------> Hom(-,FR-) | | | | | | | | Hom(FL-,epsilon-) o alpha F Hom(-,epsilon-) | | | | | | v Hom(eta,-) v Hom(FL,-) -------------------------> Hom(-,-) in which the upper and left hand maps are isomorphisms and it follows that the bottom arrow is an isomorphism iff the right hand one is.