Kerodon

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

Corollary 6.1.3.7. Let $\operatorname{\mathcal{C}}$ be a $2$-category, let $f: C \rightarrow D$ and $g: D \rightarrow C$ be $2$-morphisms of $\operatorname{\mathcal{C}}$, and let $(\eta , \epsilon )$ be an adjunction between $f$ and $g$. Let $f': C \rightarrow D$ be another $1$-morphism of $\operatorname{\mathcal{C}}$. Then:

$(1)$

For every $2$-morphism $\eta ': \operatorname{id}_{C} \Rightarrow g \circ f'$, there is a unique $2$-morphism $\beta : f \Rightarrow f'$ for which $\eta '$ is equal to the composition $\operatorname{id}_{C} \xRightarrow {\eta } g \circ f \xRightarrow {\operatorname{id}_ g \circ \beta } g \circ f'$. Moreover, $\beta $ is an isomorphism if and only if $\eta '$ is the unit of an adjunction.

$(2)$

For every $2$-morphism $\epsilon ': f' \circ g \Rightarrow \operatorname{id}_ D$, there is a unique $2$-morphism $\gamma : f' \Rightarrow f$ for which $\epsilon '$ factors as a composition $f' \circ g \xRightarrow {\gamma \circ \operatorname{id}_ g} f \circ g \xRightarrow {\epsilon } \operatorname{id}_ D$. Moreover, $\gamma $ is an isomorphism if and only $\epsilon '$ is the counit of an adjunction.

Proof. Apply Corollary 6.1.3.7 to the opposite $2$-category $\operatorname{\mathcal{C}}^{\operatorname{op}}$. $\square$