Natural transformations have mates under a pair of adjunctions

Whiskering shows that the three factors defining ${\alpha }^{\mathrm{♭}}$ have successive types $HG\to G^{\mathrm{\prime }}{F}^{\mathrm{\prime }}HG\to G^{\mathrm{\prime }}KFG\to G^{\mathrm{\prime }}K$; the three factors defining ${\beta }^{\mathrm{♯}}$ have successive types $F^{\mathrm{\prime }}H\to F^{\mathrm{\prime }}HGF\to F^{\mathrm{\prime }}{G}^{\mathrm{\prime }}KF\to KF$.

Each of those six factors is a whiskering of one of ${\eta }^{\mathrm{\prime }}$, $\alpha$, $\epsilon$, ${\epsilon }^{\mathrm{\prime }}$, $\beta$, $\eta$, every one of which is natural by [L1] and the hypothesis on $\alpha$ and $\beta$; so each factor is natural by [L2], and the two vertical composites are natural by [L3]. Only the unit–counit data enters, so the argument applies whether or not the four categories are locally small.

When the two adjunctions coincide and $H,K$ are identity functors, the middle factor $G{1}_{F}G$ is the identity transformation of $GFG$, so the mate of $1_F$ is $(G\epsilon )\circ (\eta G)$, which is $1_G$ by the triangle identity of [L1]. For a typed vertical or horizontal pasting, expand the displayed formulas; interchange identifies the expansion with the corresponding pasting of the mates, with the order fixed by the types.

Substitute ${\alpha }^{\mathrm{♭}}$ into the formula for $(-{)}^{\mathrm{♯}}$. Interchange moves the two unit-counit pairs together, and the triangle identities cancel both pairs, leaving $\alpha$.

Substituting ${\beta }^{\mathrm{♯}}$ into the formula for $(-{)}^{\mathrm{♭}}$ gives the dual cancellation and leaves $\beta$. Thus the constructions are inverse.

Hence the formulas give the asserted bijection, carry $1_F$ to $1_G$ in the coinciding-adjunction case, and preserve both forms of compatible pasting.