Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$

Corollary 6.1.5.4. Let $\operatorname{\mathcal{C}}$ be a $2$-category containing objects $C$, $D$, and $E$, together with $1$-morphisms

\[ f: C \rightarrow D \quad \quad g: D \rightarrow C \quad \quad f': D \rightarrow E \quad \quad g': E \rightarrow D \]

and $2$-morphisms $\eta : \operatorname{id}_{C} \Rightarrow g \circ f$ and $\eta ': \operatorname{id}_{D} \Rightarrow g' \circ f'$. If $\eta $ and $\eta '$ are units of adjunctions, then the contraction $c(\eta ,\eta '): \operatorname{id}_{C} \Rightarrow (g \circ g') \circ (f' \circ f)$ is also the unit of an adjunction.

Proof. Combine Proposition 6.1.5.3 with the criterion of Proposition 6.1.2.9. $\square$