Composition of adjunctions in a (weak) 2-category

Question

Let $(f_1, g_1, \varepsilon_1, \eta_1)$ and $(f_2, g_2, \varepsilon_2, \eta_2)$ be adjunctions in a (weak) 2-category. Then there is an adjunction $(f_2 \circ f1, g1 \circ g2, \varepsilon, \eta)$. I can figure out how to define $\varepsilon$ (resp., $\eta$) by inserting appropriately the unitors and associators between $\varepsilon_1$ and $\varepsilon_2$ (resp., $\eta_1$ and $\eta_2$).

Although I know how to prove the counit-unit equations in the special case of the 2-category of categories (See for instance this answer), I cannot figure out how to prove them in the general case.

Could someone spell out the commutative diagrams or provide with a reference where it is done in full?

It is stated in Section 2.1 of Review of the elements of 2-categories (Kelly and Street, 1974), but there is unfortunately no proof there.

Answer 1

In a 2-category a 2-cell $\alpha : U \Rightarrow V$ can be whiskered with a 1-cell $F$ on the right or on the left (of course, domains and codomains must match appropriately), to give $\alpha *F$ and $F * \alpha$ (refer to Borceux I for the notation and the properties of whiskering, or "Review of the elements of 2-categories", by Kelly and Street).

The whiskering of a 2-cell $\alpha$ with a composition of functors $HK$ satisfies $\alpha * HK = (\alpha *H)*K $, and similarly $(\beta \circ \alpha)*H = (\beta *H)\circ (\alpha *H)$. [1]

The whiskering operation allows you to state the zig-zag identities for the co/unit of an adjunction: if $F\dashv G$, then $(\epsilon * F ) \circ (F * \eta) = 1_F$ and $(G * \epsilon)\circ (\eta * G)=1_G$.

Now for the proof: the counit of the composite adjunction $F = F_2F_1\dashv G_1G_2 =G$ is the 2-cell $F_2F_1G_1G_2 \overset{F_2 * \epsilon_1 * G_2}\Rightarrow F_2G_2 \overset{\epsilon_2}\Rightarrow 1$, and the unit is $1 \overset{\eta_1}\Rightarrow G_1F_1 \overset{G_1 *\eta_2 * F_1}\Rightarrow G_1G_2F_2F_1$.

I'll just start half of the proof :-) go on yourself!

$$ \begin{align*} (\epsilon * F ) \circ (F * \eta) &= ((\epsilon_2 \circ (F_2 * \epsilon_1 * G_2))*F)\circ (F * ((G_1 *\eta_2 * F_1)\circ \eta_1)) \\ [1]&=\epsilon_2F_2F_1 \circ F_2\epsilon_1G_2F_2F_1 \circ F_2F_1G_2\eta_2F_1\circ F_2F_1\eta_1 \end{align*} $$

Answer 2

Analogously to the case of Sets in 1-category theory, it’s often enough to prove a statement for categories and apply the Yoneda embedding. This maps an adjunction in $K$ to an adjunction in the 2-category of 2-functors $K^{op}\to Cat$. Since the 2-Yoneda embedding is 2-fully faithful, it’s enough to prove the triangle identities for the composition in the latter 2-category. And here the definition is given levelwise by the definition in Cat, so if you can prove the triangle identities in Cat, you’ve proved them in $K$!