How to prove adjunctions compose (via units and counits)?

Familiar background (partly to fix notation). Suppose we have functors $F\colon \mathscr{A} \to \mathscr{B}$, $G\colon \mathscr{B} \to \mathscr{A}$ such that $F \dashv G$, and functors $F'\colon \mathscr{B} \to \mathscr{C}$, $G'\colon \mathscr{C} \to \mathscr{B}$ such that $F' \dashv G'$. We want to prove the adjunctions compose, so $F'F \dashv GG'$.

One way is to do it via homsets.

Another is via units and counits. Suppose $\eta, \varepsilon$ are the unit and counit of the first adjunction, and $\eta', \varepsilon'$ the unit and counit of the second adjunction. Then we evidently have natural transformations $\eta'', \varepsilon''$ defined by composition as follows: $$\eta'': \quad 1_{\mathscr{A}}\overset{\eta}\Longrightarrow GF \overset{G\eta'F}\Longrightarrow GG'F'F$$ $$\varepsilon'': \quad F'FGG' \overset{F'\epsilon G'}\Longrightarrow F'G' \overset{\varepsilon'}\Longrightarrow 1_{\mathscr{C}}$$ So to complete the proof that $F'F \dashv GG'$ it "just" remains to show by a diagram chase that $\eta'', \varepsilon''$ are a unit and counit for this adjunction because they satisfy the triangle equalities.

Mac Lane in effect sets this as an exercise for the reader at the bottom of p. 103 of Categories for the Working Mathematician. But this reader seems to be having a senior moment (well, a few moments), which is why I am asking here the embarrassingly undergraduate ...

Question How does the diagram chase for one of the required triangle equalities actually go?

• The most intuitive argument goes via string diagrams, by the way. String diagrams make the problem of "seeing naturality squares" disappear. They are helpful in a lot of 2-categorical concepts.
– user158047
Jun 8, 2015 at 8:50

$\begin{array}{ccccc} F'F & \underset{F'F\eta}{\rightarrow} & F'FGF & \underset{F'FG\eta'F}{\rightarrow} & F'FGG'F'F \\ & \searrow & \downarrow^{F'\varepsilon F} & & \downarrow^{F'\varepsilon G'F'F} \\ & & F'F & \underset{F'\eta'F}{\rightarrow} & F'G'F'F \\ & & & \searrow & \downarrow^{\varepsilon' F'F} \\ & & & & F'F \end{array}$
The two triangles come from the triangle identities for $F\dashv G$ and $F' \dashv G'$, and the square commutes by naturality of either $\eta'$ or $\varepsilon$.
• Just to add something I find useful when dealing with these kinds of situations: a good way to not miss that naturality square is to note that the two transformation at the junction are "acting past each other": $η'$ inserts the $G'F'$ into the $F'FGG'F'F$, while $ε$ collapses the completely unrelated $FG$. This means that $F'εG'F'F ∘ F'FGη'F$ is equal to the horizontal composite $F'εη'F$, and these can always be written in two ways. Jun 6, 2015 at 22:11