[proofplan] We define $F$ on morphisms by applying the universal property of $\eta_c$ to the composite $\eta_{c'}\circ u:c\to G(Fc')$. The identity and composition axioms follow from the uniqueness clause in the same universal property. The adjunction is then obtained from the universal bijection sending $a:Fc\to d$ to $G(a)\circ\eta_c$, and naturality follows by comparing both sides with the defining equations for $F$ and functoriality of $G$. [/proofplan] [step:Define the action of $F$ on morphisms using the universal arrows] Let $u:c\to c'$ be a morphism in $\mathcal{C}$. The composite \begin{align*} \eta_{c'}\circ u:c\to G(Fc') \end{align*} is a morphism from $c$ to the $G$-image of the object $Fc'\in\mathcal{D}$. Applying the universal property of $\eta_c:c\to G(Fc)$ with $d=Fc'$ and $f=\eta_{c'}\circ u$, there is a unique morphism \begin{align*} Fu:Fc\to Fc' \end{align*} in $\mathcal{D}$ such that \begin{align*} G(Fu)\circ \eta_c=\eta_{c'}\circ u. \end{align*} This defines the value of $F$ on every morphism of $\mathcal{C}$. [guided] We already have an object assignment $c\mapsto Fc$. To make it into a functor, we must define what happens to a morphism $u:c\to c'$. The universal arrow at $c$ gives a way to factor every morphism from $c$ into an object of the form $Gd$ uniquely through $\eta_c$. For the morphism $u:c\to c'$, the target $c'$ has its own chosen universal arrow $\eta_{c'}:c'\to G(Fc')$. Therefore the composite \begin{align*} \eta_{c'}\circ u:c\to G(Fc') \end{align*} has exactly the form required by the universal property of $\eta_c$, with $d=Fc'$. Hence there exists a unique morphism \begin{align*} Fu:Fc\to Fc' \end{align*} such that \begin{align*} G(Fu)\circ \eta_c=\eta_{c'}\circ u. \end{align*} This equation is the defining equation for $Fu$. Every later verification will reduce to showing that some candidate morphism satisfies this same equation, so that uniqueness forces it to equal $Fu$. [/guided] [/step] [step:Verify that $F$ preserves identity morphisms] Let $c\in\mathcal{C}$. By the definition of $F(\operatorname{id}_c)$, the morphism \begin{align*} F(\operatorname{id}_c):Fc\to Fc \end{align*} is the unique morphism satisfying \begin{align*} G(F(\operatorname{id}_c))\circ \eta_c=\eta_c\circ \operatorname{id}_c=\eta_c. \end{align*} The identity morphism $\operatorname{id}_{Fc}:Fc\to Fc$ also satisfies this equation, since $G(\operatorname{id}_{Fc})=\operatorname{id}_{G(Fc)}$. Therefore uniqueness gives \begin{align*} F(\operatorname{id}_c)=\operatorname{id}_{Fc}. \end{align*} [/step] [step:Verify that $F$ preserves composition] Let $u:c\to c'$ and $v:c'\to c''$ be morphisms in $\mathcal{C}$. By definition, $F(v\circ u):Fc\to Fc''$ is the unique morphism satisfying \begin{align*} G(F(v\circ u))\circ \eta_c=\eta_{c''}\circ v\circ u. \end{align*} We show that the composite $Fv\circ Fu:Fc\to Fc''$ satisfies the same equation. Using functoriality of $G$ and the defining equations for $Fu$ and $Fv$, we compute \begin{align*} G(Fv\circ Fu)\circ \eta_c &=G(Fv)\circ G(Fu)\circ \eta_c \\ &=G(Fv)\circ \eta_{c'}\circ u \\ &=\eta_{c''}\circ v\circ u. \end{align*} Thus $Fv\circ Fu$ satisfies the defining equation for $F(v\circ u)$, and uniqueness gives \begin{align*} F(v\circ u)=Fv\circ Fu. \end{align*} Together with preservation of identities, this proves that $F:\mathcal{C}\to\mathcal{D}$ is a functor. [guided] To prove functoriality, we must show that the morphism assigned to a composite is the composite of the assigned morphisms. Let \begin{align*} u:c\to c', \qquad v:c'\to c'' \end{align*} be morphisms in $\mathcal{C}$. The defining property of $F(v\circ u)$ says that it is the unique morphism $Fc\to Fc''$ whose image under $G$, after precomposition with $\eta_c$, equals $\eta_{c''}\circ v\circ u$: \begin{align*} G(F(v\circ u))\circ \eta_c=\eta_{c''}\circ v\circ u. \end{align*} Now test the candidate $Fv\circ Fu:Fc\to Fc''$. Since $G$ is a functor, it preserves composition, so \begin{align*} G(Fv\circ Fu)=G(Fv)\circ G(Fu). \end{align*} Therefore \begin{align*} G(Fv\circ Fu)\circ \eta_c &=G(Fv)\circ G(Fu)\circ \eta_c \\ &=G(Fv)\circ \eta_{c'}\circ u \\ &=\eta_{c''}\circ v\circ u. \end{align*} The second equality uses the defining equation for $Fu$, and the third equality uses the defining equation for $Fv$. Thus $Fv\circ Fu$ and $F(v\circ u)$ satisfy the same universal factoring equation. The universal property of $\eta_c$ gives uniqueness of such a morphism $Fc\to Fc''$, so \begin{align*} F(v\circ u)=Fv\circ Fu. \end{align*} Hence $F$ preserves composition. [/guided] [/step] [step:Construct the adjunction bijections from the universal property] For objects $c\in\mathcal{C}$ and $d\in\mathcal{D}$, define a function \begin{align*} \Phi_{c,d}:\mathcal{D}(Fc,d)&\to \mathcal{C}(c,Gd)\\ a&\mapsto G(a)\circ \eta_c. \end{align*} The universal property of $\eta_c$ says precisely that for every morphism $f:c\to Gd$ there exists a unique morphism $a:Fc\to d$ such that $\Phi_{c,d}(a)=f$. Therefore $\Phi_{c,d}$ is bijective for every pair $(c,d)$. [guided] The universal arrow at $c$ does more than define $F$ on morphisms: it gives the hom-set bijection required for an adjunction. Fix objects $c\in\mathcal{C}$ and $d\in\mathcal{D}$. Define \begin{align*} \Phi_{c,d}:\mathcal{D}(Fc,d)&\to \mathcal{C}(c,Gd)\\ a&\mapsto G(a)\circ \eta_c. \end{align*} This function sends a morphism $a:Fc\to d$ in $\mathcal{D}$ to the corresponding morphism $c\to Gd$ in $\mathcal{C}$ obtained by first applying the universal arrow $\eta_c:c\to G(Fc)$ and then applying $G(a):G(Fc)\to Gd$. The universal property of $\eta_c$ says that every morphism $f:c\to Gd$ factors in exactly one way through $\eta_c$ by a morphism $a:Fc\to d$: \begin{align*} G(a)\circ \eta_c=f. \end{align*} Existence gives surjectivity of $\Phi_{c,d}$, and uniqueness gives injectivity. Hence $\Phi_{c,d}$ is a bijection. [/guided] [/step] [step:Prove naturality of the adjunction bijections] Let $u:c'\to c$ be a morphism in $\mathcal{C}$ and let $a:Fc\to d$ be a morphism in $\mathcal{D}$. Naturality in the $\mathcal{C}$-variable requires \begin{align*} \Phi_{c',d}(a\circ Fu)=\Phi_{c,d}(a)\circ u. \end{align*} Using the definition of $\Phi$ and the defining equation for $Fu$, we have \begin{align*} \Phi_{c',d}(a\circ Fu) &=G(a\circ Fu)\circ \eta_{c'}\\ &=G(a)\circ G(Fu)\circ \eta_{c'}\\ &=G(a)\circ \eta_c\circ u\\ &=\Phi_{c,d}(a)\circ u. \end{align*} Let $b:d\to d'$ be a morphism in $\mathcal{D}$ and let $a:Fc\to d$ be a morphism in $\mathcal{D}$. Naturality in the $\mathcal{D}$-variable requires \begin{align*} \Phi_{c,d'}(b\circ a)=G(b)\circ \Phi_{c,d}(a). \end{align*} By functoriality of $G$, \begin{align*} \Phi_{c,d'}(b\circ a) &=G(b\circ a)\circ \eta_c\\ &=G(b)\circ G(a)\circ \eta_c\\ &=G(b)\circ \Phi_{c,d}(a). \end{align*} Thus the bijections $\Phi_{c,d}$ are natural in both variables, so they define an adjunction $F\dashv G$. [guided] An adjunction is not just a family of bijections; the bijections must be natural in both variables. First fix a morphism \begin{align*} u:c'\to c \end{align*} in $\mathcal{C}$ and a morphism \begin{align*} a:Fc\to d \end{align*} in $\mathcal{D}$. Naturality in the $\mathcal{C}$-variable says that precomposing $G(a)\circ\eta_c$ by $u$ should match first moving $a$ along $Fu:Fc'\to Fc$ and then applying the bijection. Compute: \begin{align*} \Phi_{c',d}(a\circ Fu) &=G(a\circ Fu)\circ \eta_{c'}\\ &=G(a)\circ G(Fu)\circ \eta_{c'}\\ &=G(a)\circ \eta_c\circ u\\ &=\Phi_{c,d}(a)\circ u. \end{align*} The second equality uses functoriality of $G$, and the third equality is the defining equation for $Fu$ applied to the morphism $u:c'\to c$. Now fix a morphism \begin{align*} b:d\to d' \end{align*} in $\mathcal{D}$ and keep $a:Fc\to d$. Naturality in the $\mathcal{D}$-variable says that postcomposing $a$ by $b$ before applying $\Phi$ is the same as applying $\Phi$ first and then postcomposing by $G(b)$. This follows directly from functoriality: \begin{align*} \Phi_{c,d'}(b\circ a) &=G(b\circ a)\circ \eta_c\\ &=G(b)\circ G(a)\circ \eta_c\\ &=G(b)\circ \Phi_{c,d}(a). \end{align*} Therefore the bijections $\Phi_{c,d}$ are natural in both variables, and they define an adjunction $F\dashv G$. [/guided] [/step] [step:Identify $\eta$ as the unit and prove uniqueness of the functor] Under the bijection \begin{align*} \Phi_{c,Fc}:\mathcal{D}(Fc,Fc)\to \mathcal{C}(c,G(Fc)), \end{align*} the identity morphism $\operatorname{id}_{Fc}:Fc\to Fc$ maps to \begin{align*} \Phi_{c,Fc}(\operatorname{id}_{Fc}) =G(\operatorname{id}_{Fc})\circ \eta_c =\operatorname{id}_{G(Fc)}\circ \eta_c =\eta_c. \end{align*} Hence the unit of the adjunction $F\dashv G$ is exactly the family $\eta=(\eta_c)_{c\in\mathcal{C}}$. Finally, suppose $F':\mathcal{C}\to\mathcal{D}$ is another functor with the same object assignment $F'c=Fc$ and satisfying \begin{align*} G(F'u)\circ \eta_c=\eta_{c'}\circ u \end{align*} for every morphism $u:c\to c'$ in $\mathcal{C}$. For each such $u$, both $F'u$ and $Fu$ are morphisms $Fc\to Fc'$ satisfying the same universal factoring equation through $\eta_c$. By uniqueness in the universal property of $\eta_c$, \begin{align*} F'u=Fu. \end{align*} Thus the extension of the object assignment to a functor satisfying the displayed defining equation is unique. This completes the proof. [/step]