[proofplan] The converse direction is formal: an adjunction whose unit and counit are natural isomorphisms already supplies the two natural isomorphisms required in the definition of equivalence. For the forward direction, we start from arbitrary equivalence data $\eta: \operatorname{id}_{\mathcal C} \Rightarrow GF$ and $\delta: FG \Rightarrow \operatorname{id}_{\mathcal D}$, keep $\eta$ fixed, and modify the counit to a new natural isomorphism $\varepsilon: FG \Rightarrow \operatorname{id}_{\mathcal D}$. The definition of $\varepsilon$ is chosen so that the triangle identity for $G$ holds by construction; naturality of $\eta$ and $\delta$ then gives the triangle identity for $F$. Once the two triangle identities are established, the usual hom-set formulas define the adjunction $F \dashv G$. [/proofplan]

[step:Extract the equivalence data and define the adjusted counit]Assume first that $F$ and $G$ form an equivalence of categories. Thus there are natural isomorphisms \begin{align*} \eta: \operatorname{id}_{\mathcal C} &\Rightarrow GF,\\ \delta: FG &\Rightarrow \operatorname{id}_{\mathcal D}. \end{align*} For each object $d \in \mathcal D$, define a morphism \begin{align*} \varepsilon_d: FGd \to d \end{align*} by \begin{align*} \varepsilon_d := \delta_d \circ F(\eta_{Gd}^{-1}) \circ \delta_{FGd}^{-1}. \end{align*} The types are as follows: \begin{align*} FGd \xrightarrow{\delta_{FGd}^{-1}} FGFGd \xrightarrow{F(\eta_{Gd}^{-1})} FGd \xrightarrow{\delta_d} d. \end{align*} Since $\delta_{FGd}$, $\eta_{Gd}$, and $\delta_d$ are isomorphisms, each $\varepsilon_d$ is an isomorphism.[/step]

[guided]We begin with an equivalence of categories. This means that $F$ and $G$ are already quasi-inverse functors, but the given natural isomorphisms need not satisfy the triangle identities required of an adjunction. We keep the natural isomorphism \begin{align*} \eta: \operatorname{id}_{\mathcal C} \Rightarrow GF \end{align*} as the prospective unit. The given comparison \begin{align*} \delta: FG \Rightarrow \operatorname{id}_{\mathcal D} \end{align*} is not necessarily the right counit. We therefore define a new family of morphisms. For every object $d \in \mathcal D$, set \begin{align*} \varepsilon_d := \delta_d \circ F(\eta_{Gd}^{-1}) \circ \delta_{FGd}^{-1}. \end{align*} This formula is type-correct because \begin{align*} \delta_{FGd}^{-1}&: FGd \to FGFGd,\\ F(\eta_{Gd}^{-1})&: FGFGd \to FGd,\\ \delta_d&: FGd \to d. \end{align*} Thus the composite is a morphism $\varepsilon_d: FGd \to d$. Each factor is an isomorphism, so $\varepsilon_d$ is also an isomorphism.[/guided]

[step:Verify that the adjusted counit is natural]Let $h: d \to d'$ be a morphism in $\mathcal D$. We prove \begin{align*} h \circ \varepsilon_d = \varepsilon_{d'} \circ FGh. \end{align*} Using the definition of $\varepsilon_d$ and naturality of $\delta$ at $h$, naturality of $\delta$ at $FGh$, and naturality of $\eta^{-1}$ at $Gh$, we compute \begin{align*} h \circ \varepsilon_d &= h \circ \delta_d \circ F(\eta_{Gd}^{-1}) \circ \delta_{FGd}^{-1}\\ &= \delta_{d'} \circ FGh \circ F(\eta_{Gd}^{-1}) \circ \delta_{FGd}^{-1}\\ &= \delta_{d'} \circ F(Gh \circ \eta_{Gd}^{-1}) \circ \delta_{FGd}^{-1}\\ &= \delta_{d'} \circ F(\eta_{Gd'}^{-1} \circ GFGh) \circ \delta_{FGd}^{-1}\\ &= \delta_{d'} \circ F(\eta_{Gd'}^{-1}) \circ FGFGh \circ \delta_{FGd}^{-1}\\ &= \delta_{d'} \circ F(\eta_{Gd'}^{-1}) \circ \delta_{FGd'}^{-1} \circ FGh\\ &= \varepsilon_{d'} \circ FGh. \end{align*} Hence $\varepsilon: FG \Rightarrow \operatorname{id}_{\mathcal D}$ is a natural isomorphism.[/step]

[guided]To prove that $\varepsilon$ is natural, we must show that every morphism $h: d \to d'$ in $\mathcal D$ makes the square for $\varepsilon: FG \Rightarrow \operatorname{id}_{\mathcal D}$ commute. Equivalently, we must prove \begin{align*} h \circ \varepsilon_d = \varepsilon_{d'} \circ FGh. \end{align*} Substitute the definition of $\varepsilon_d$: \begin{align*} h \circ \varepsilon_d &= h \circ \delta_d \circ F(\eta_{Gd}^{-1}) \circ \delta_{FGd}^{-1}. \end{align*} Naturality of $\delta$ applied to $h: d \to d'$ gives \begin{align*} h \circ \delta_d = \delta_{d'} \circ FGh. \end{align*} Therefore \begin{align*} h \circ \varepsilon_d &= \delta_{d'} \circ FGh \circ F(\eta_{Gd}^{-1}) \circ \delta_{FGd}^{-1}\\ &= \delta_{d'} \circ F(Gh \circ \eta_{Gd}^{-1}) \circ \delta_{FGd}^{-1}. \end{align*} Naturality of the inverse natural transformation $\eta^{-1}: GF \Rightarrow \operatorname{id}_{\mathcal C}$ applied to $Gh: Gd \to Gd'$ gives \begin{align*} Gh \circ \eta_{Gd}^{-1} = \eta_{Gd'}^{-1} \circ GFGh. \end{align*} Using this identity inside $F$ gives \begin{align*} h \circ \varepsilon_d &= \delta_{d'} \circ F(\eta_{Gd'}^{-1} \circ GFGh) \circ \delta_{FGd}^{-1}\\ &= \delta_{d'} \circ F(\eta_{Gd'}^{-1}) \circ FGFGh \circ \delta_{FGd}^{-1}. \end{align*} Finally, naturality of $\delta$ applied to $FGh: FGd \to FGd'$ gives \begin{align*} FGh \circ \delta_{FGd} = \delta_{FGd'} \circ FGFGh. \end{align*} Since each component of $\delta$ is an isomorphism, this is equivalent to \begin{align*} FGFGh \circ \delta_{FGd}^{-1} = \delta_{FGd'}^{-1} \circ FGh. \end{align*} Substituting this into the previous composite yields \begin{align*} h \circ \varepsilon_d &= \delta_{d'} \circ F(\eta_{Gd'}^{-1}) \circ \delta_{FGd'}^{-1} \circ FGh\\ &= \varepsilon_{d'} \circ FGh. \end{align*} Thus $\varepsilon$ is natural. Since each component $\varepsilon_d$ is already known to be an isomorphism, $\varepsilon$ is a natural isomorphism.[/guided]

[step:Prove the triangle identity for $G$]For each object $d \in \mathcal D$, we prove \begin{align*} G\varepsilon_d \circ \eta_{Gd} = \operatorname{id}_{Gd}. \end{align*} Naturality of $\delta$ applied to the morphism $\delta_d^{-1}: d \to FGd$ gives \begin{align*} \delta_d^{-1} \circ \delta_d = \delta_{FGd} \circ FG(\delta_d^{-1}). \end{align*} Since $\delta_d^{-1} \circ \delta_d = \operatorname{id}_{FGd}$, this gives \begin{align*} FG(\delta_d^{-1}) = \delta_{FGd}^{-1}. \end{align*} Applying $G$ yields \begin{align*} GFG(\delta_d^{-1}) = G(\delta_{FGd}^{-1}). \end{align*} Naturality of $\eta$ applied to the morphism $G(\delta_d^{-1}): Gd \to GFGd$ gives \begin{align*} GFG(\delta_d^{-1}) \circ \eta_{Gd} = \eta_{GFGd} \circ G(\delta_d^{-1}). \end{align*} Naturality of $\eta$ applied to the morphism $\eta_{Gd}^{-1}: GFGd \to Gd$ gives \begin{align*} GF(\eta_{Gd}^{-1}) \circ \eta_{GFGd} = \eta_{Gd} \circ \eta_{Gd}^{-1} = \operatorname{id}_{GFGd}. \end{align*} Applying $G$ to the definition of $\varepsilon_d$ and composing with $\eta_{Gd}$ gives \begin{align*} G\varepsilon_d \circ \eta_{Gd} &= G(\delta_d) \circ GF(\eta_{Gd}^{-1}) \circ G(\delta_{FGd}^{-1}) \circ \eta_{Gd}\\ &= G(\delta_d) \circ GF(\eta_{Gd}^{-1}) \circ GFG(\delta_d^{-1}) \circ \eta_{Gd}\\ &= G(\delta_d) \circ GF(\eta_{Gd}^{-1}) \circ \eta_{GFGd} \circ G(\delta_d^{-1})\\ &= G(\delta_d) \circ G(\delta_d^{-1})\\ &= \operatorname{id}_{Gd}. \end{align*} Thus the $G$-triangle identity holds.[/step]

[guided]The delicate point is that $\eta$ is a natural transformation on $\mathcal C$, so it may only be applied to morphisms in $\mathcal C$. The morphism $\delta_d: FGd \to d$ lies in $\mathcal D$, so we first convert it into a morphism in $\mathcal C$ by applying $G$ to the inverse $\delta_d^{-1}: d \to FGd$. Naturality of $\delta: FG \Rightarrow \operatorname{id}_{\mathcal D}$ applied to $\delta_d^{-1}: d \to FGd$ says \begin{align*} \delta_d^{-1} \circ \delta_d = \delta_{FGd} \circ FG(\delta_d^{-1}). \end{align*} The left-hand side is $\operatorname{id}_{FGd}$ because $\delta_d$ is an isomorphism. Hence \begin{align*} FG(\delta_d^{-1}) = \delta_{FGd}^{-1}. \end{align*} After applying the functor $G$, this becomes \begin{align*} GFG(\delta_d^{-1}) = G(\delta_{FGd}^{-1}). \end{align*} Now apply naturality of $\eta: \operatorname{id}_{\mathcal C} \Rightarrow GF$ to the morphism $G(\delta_d^{-1}): Gd \to GFGd$ in $\mathcal C$. This gives \begin{align*} GFG(\delta_d^{-1}) \circ \eta_{Gd} = \eta_{GFGd} \circ G(\delta_d^{-1}). \end{align*} We also apply naturality of $\eta$ to the morphism $\eta_{Gd}^{-1}: GFGd \to Gd$. The result is \begin{align*} GF(\eta_{Gd}^{-1}) \circ \eta_{GFGd} = \eta_{Gd} \circ \eta_{Gd}^{-1} = \operatorname{id}_{GFGd}. \end{align*} These two naturality identities are exactly what the definition of $\varepsilon_d$ was designed to use. Applying $G$ to \begin{align*} \varepsilon_d = \delta_d \circ F(\eta_{Gd}^{-1}) \circ \delta_{FGd}^{-1} \end{align*} and then composing with $\eta_{Gd}$ gives \begin{align*} G\varepsilon_d \circ \eta_{Gd} &= G(\delta_d) \circ GF(\eta_{Gd}^{-1}) \circ G(\delta_{FGd}^{-1}) \circ \eta_{Gd}\\ &= G(\delta_d) \circ GF(\eta_{Gd}^{-1}) \circ GFG(\delta_d^{-1}) \circ \eta_{Gd}\\ &= G(\delta_d) \circ GF(\eta_{Gd}^{-1}) \circ \eta_{GFGd} \circ G(\delta_d^{-1})\\ &= G(\delta_d) \circ G(\delta_d^{-1})\\ &= \operatorname{id}_{Gd}. \end{align*} Thus $G\varepsilon_d \circ \eta_{Gd}=\operatorname{id}_{Gd}$ for every object $d \in \mathcal D$, which is the triangle identity for $G$.[/guided]

[step:Prove the triangle identity for $F$]For each object $c \in \mathcal C$, we prove \begin{align*} \varepsilon_{Fc} \circ F\eta_c = \operatorname{id}_{Fc}. \end{align*} By the definition of $\varepsilon$, \begin{align*} \varepsilon_{Fc} \circ F\eta_c &= \delta_{Fc} \circ F(\eta_{GFc}^{-1}) \circ \delta_{FGFc}^{-1} \circ F\eta_c. \end{align*} Naturality of $\delta$ applied to the morphism $F\eta_c: Fc \to FGFc$ gives \begin{align*} F\eta_c \circ \delta_{Fc} = \delta_{FGFc} \circ FGF\eta_c. \end{align*} After rearranging this identity through the displayed composite, it follows that \begin{align*} \delta_{FGFc}^{-1} \circ F\eta_c = FGF\eta_c \circ \delta_{Fc}^{-1}. \end{align*} Therefore \begin{align*} \varepsilon_{Fc} \circ F\eta_c &= \delta_{Fc} \circ F(\eta_{GFc}^{-1}) \circ FGF\eta_c \circ \delta_{Fc}^{-1}\\ &= \delta_{Fc} \circ F(\eta_{GFc}^{-1} \circ GF\eta_c) \circ \delta_{Fc}^{-1}. \end{align*} Naturality of $\eta$ applied to the morphism $\eta_c: c \to GFc$ gives \begin{align*} GF\eta_c \circ \eta_c = \eta_{GFc} \circ \eta_c. \end{align*} Since $\eta_c$ is an isomorphism, cancellation on the right gives \begin{align*} GF\eta_c = \eta_{GFc}. \end{align*} Hence \begin{align*} \varepsilon_{Fc} \circ F\eta_c &= \delta_{Fc} \circ F(\operatorname{id}_{GFc}) \circ \delta_{Fc}^{-1}\\ &= \operatorname{id}_{Fc}. \end{align*} Thus the $F$-triangle identity holds.[/step]

[guided]We now prove the other triangle identity. For each object $c \in \mathcal C$, the desired equality is \begin{align*} \varepsilon_{Fc} \circ F\eta_c = \operatorname{id}_{Fc}. \end{align*} Substitute the definition of the adjusted counit at the object $Fc \in \mathcal D$: \begin{align*} \varepsilon_{Fc} \circ F\eta_c &= \delta_{Fc} \circ F(\eta_{GFc}^{-1}) \circ \delta_{FGFc}^{-1} \circ F\eta_c. \end{align*} The term to simplify is $\delta_{FGFc}^{-1} \circ F\eta_c$. Naturality of $\delta: FG \Rightarrow \operatorname{id}_{\mathcal D}$ applied to the morphism $F\eta_c: Fc \to FGFc$ gives \begin{align*} F\eta_c \circ \delta_{Fc} = \delta_{FGFc} \circ FGF\eta_c. \end{align*} Composing this equality on the left by $\delta_{FGFc}^{-1}$ and on the right by $\delta_{Fc}^{-1}$ gives \begin{align*} \delta_{FGFc}^{-1} \circ F\eta_c = FGF\eta_c \circ \delta_{Fc}^{-1}. \end{align*} Substituting into the displayed composite yields \begin{align*} \varepsilon_{Fc} \circ F\eta_c &= \delta_{Fc} \circ F(\eta_{GFc}^{-1}) \circ FGF\eta_c \circ \delta_{Fc}^{-1}\\ &= \delta_{Fc} \circ F(\eta_{GFc}^{-1} \circ GF\eta_c) \circ \delta_{Fc}^{-1}. \end{align*} It remains to identify the middle composite in $\mathcal C$. Naturality of $\eta: \operatorname{id}_{\mathcal C} \Rightarrow GF$ applied to $\eta_c: c \to GFc$ gives \begin{align*} GF\eta_c \circ \eta_c = \eta_{GFc} \circ \eta_c. \end{align*} Because $\eta_c$ is an isomorphism, we may cancel it on the right and obtain \begin{align*} GF\eta_c = \eta_{GFc}. \end{align*} Therefore \begin{align*} \eta_{GFc}^{-1} \circ GF\eta_c = \operatorname{id}_{GFc}. \end{align*} Substitution gives \begin{align*} \varepsilon_{Fc} \circ F\eta_c &= \delta_{Fc} \circ F(\operatorname{id}_{GFc}) \circ \delta_{Fc}^{-1}\\ &= \delta_{Fc} \circ \operatorname{id}_{FGFc} \circ \delta_{Fc}^{-1}\\ &= \operatorname{id}_{Fc}. \end{align*} Thus $\varepsilon_{Fc} \circ F\eta_c=\operatorname{id}_{Fc}$ for every object $c \in \mathcal C$, which is the triangle identity for $F$.[/guided]

[step:Construct the adjunction from the two triangle identities]For objects $c \in \mathcal C$ and $d \in \mathcal D$, define maps between hom-sets \begin{align*} \Phi_{c,d}: \operatorname{Hom}_{\mathcal D}(Fc,d) &\to \operatorname{Hom}_{\mathcal C}(c,Gd),\\ f &\mapsto Gf \circ \eta_c, \end{align*} and \begin{align*} \Psi_{c,d}: \operatorname{Hom}_{\mathcal C}(c,Gd) &\to \operatorname{Hom}_{\mathcal D}(Fc,d),\\ g &\mapsto \varepsilon_d \circ Fg. \end{align*} For $f: Fc \to d$, \begin{align*} \Psi_{c,d}(\Phi_{c,d}(f)) &= \varepsilon_d \circ F(Gf \circ \eta_c)\\ &= \varepsilon_d \circ FGf \circ F\eta_c\\ &= f \circ \varepsilon_{Fc} \circ F\eta_c\\ &= f. \end{align*} The third equality is naturality of $\varepsilon$ applied to $f: Fc \to d$, and the fourth equality is the $F$-triangle identity. For $g: c \to Gd$, \begin{align*} \Phi_{c,d}(\Psi_{c,d}(g)) &= G(\varepsilon_d \circ Fg) \circ \eta_c\\ &= G\varepsilon_d \circ GFg \circ \eta_c\\ &= G\varepsilon_d \circ \eta_{Gd} \circ g\\ &= g. \end{align*} The third equality is naturality of $\eta$ applied to $g: c \to Gd$, and the fourth equality is the $G$-triangle identity. Hence $\Phi_{c,d}$ is a bijection with inverse $\Psi_{c,d}$. We verify naturality in both variables. If $a: c' \to c$ is a morphism in $\mathcal C$ and $f: Fc \to d$ is a morphism in $\mathcal D$, then naturality of $\eta$ at $a$ gives \begin{align*} \Phi_{c',d}(f \circ Fa) &= G(f \circ Fa) \circ \eta_{c'}\\ &= Gf \circ GFa \circ \eta_{c'}\\ &= Gf \circ \eta_c \circ a\\ &= \Phi_{c,d}(f) \circ a. \end{align*} If $b: d \to d'$ is a morphism in $\mathcal D$, then functoriality of $G$ gives \begin{align*} \Phi_{c,d'}(b \circ f) &= G(b \circ f) \circ \eta_c\\ &= Gb \circ Gf \circ \eta_c\\ &= Gb \circ \Phi_{c,d}(f). \end{align*} Thus $\Phi$ is natural in $c$ and $d$. These natural hom-set bijections are the standard hom-set characterization of an [adjunction](/page/Adjunction), with unit $\eta$ and counit $\varepsilon$ because the defining formulas are $f \mapsto Gf \circ \eta_c$ and $g \mapsto \varepsilon_d \circ Fg$. Therefore $F \dashv G$ with unit $\eta$ and counit $\varepsilon$, and both are natural isomorphisms.[/step]

[guided]We now build the adjunction from the unit-counit data. For objects $c \in \mathcal C$ and $d \in \mathcal D$, define maps between hom-sets by \begin{align*} \Phi_{c,d}: \operatorname{Hom}_{\mathcal D}(Fc,d) &\to \operatorname{Hom}_{\mathcal C}(c,Gd),\\ f &\mapsto Gf \circ \eta_c, \end{align*} and \begin{align*} \Psi_{c,d}: \operatorname{Hom}_{\mathcal C}(c,Gd) &\to \operatorname{Hom}_{\mathcal D}(Fc,d),\\ g &\mapsto \varepsilon_d \circ Fg. \end{align*} We first prove that these maps are inverse bijections. Let $f: Fc \to d$ be a morphism in $\mathcal D$. Then \begin{align*} \Psi_{c,d}(\Phi_{c,d}(f)) &= \varepsilon_d \circ F(Gf \circ \eta_c)\\ &= \varepsilon_d \circ FGf \circ F\eta_c\\ &= f \circ \varepsilon_{Fc} \circ F\eta_c\\ &= f. \end{align*} The third equality is naturality of $\varepsilon: FG \Rightarrow \operatorname{id}_{\mathcal D}$ applied to $f: Fc \to d$, and the fourth equality is the $F$-triangle identity. Let $g: c \to Gd$ be a morphism in $\mathcal C$. Then \begin{align*} \Phi_{c,d}(\Psi_{c,d}(g)) &= G(\varepsilon_d \circ Fg) \circ \eta_c\\ &= G\varepsilon_d \circ GFg \circ \eta_c\\ &= G\varepsilon_d \circ \eta_{Gd} \circ g\\ &= g. \end{align*} The third equality is naturality of $\eta: \operatorname{id}_{\mathcal C} \Rightarrow GF$ applied to $g: c \to Gd$, and the fourth equality is the $G$-triangle identity. Hence $\Phi_{c,d}$ and $\Psi_{c,d}$ are inverse bijections. We must also verify that the bijection is natural in both variables. Let $a: c' \to c$ be a morphism in $\mathcal C$ and let $f: Fc \to d$ be a morphism in $\mathcal D$. Naturality in the $\mathcal C$-variable means compatibility with precomposition by $a$ on the right and by $Fa$ on the left. Using naturality of $\eta$ at $a$, we compute \begin{align*} \Phi_{c',d}(f \circ Fa) &= G(f \circ Fa) \circ \eta_{c'}\\ &= Gf \circ GFa \circ \eta_{c'}\\ &= Gf \circ \eta_c \circ a\\ &= \Phi_{c,d}(f) \circ a. \end{align*} Now let $b: d \to d'$ be a morphism in $\mathcal D$. Naturality in the $\mathcal D$-variable means compatibility with postcomposition by $b$ and by $Gb$. By functoriality of $G$, \begin{align*} \Phi_{c,d'}(b \circ f) &= G(b \circ f) \circ \eta_c\\ &= Gb \circ Gf \circ \eta_c\\ &= Gb \circ \Phi_{c,d}(f). \end{align*} Thus the family $\Phi_{c,d}$ is natural in $c$ and $d$. The standard hom-set characterization of an [adjunction](/page/Adjunction) says that natural bijections \begin{align*} \operatorname{Hom}_{\mathcal D}(Fc,d) \cong \operatorname{Hom}_{\mathcal C}(c,Gd) \end{align*} are equivalent to an adjunction $F \dashv G$. The formulas above show that the associated unit is $\eta$ and the associated counit is $\varepsilon$. Since $\eta$ was given as a natural isomorphism and $\varepsilon$ was constructed as a natural isomorphism, this adjunction is an adjoint equivalence.[/guided]

[step:Recover an equivalence from an adjunction with invertible unit and counit]Conversely, suppose $F \dashv G$ has unit \begin{align*} \eta: \operatorname{id}_{\mathcal C} \Rightarrow GF \end{align*} and counit \begin{align*} \varepsilon: FG \Rightarrow \operatorname{id}_{\mathcal D}, \end{align*} and suppose both $\eta$ and $\varepsilon$ are natural isomorphisms. These are exactly the natural isomorphisms required to exhibit $G$ as a quasi-inverse to $F$. Hence $F$ and $G$ form an equivalence of categories.[/step]

[guided]For the converse direction, assume that $F \dashv G$ has unit \begin{align*} \eta: \operatorname{id}_{\mathcal C} \Rightarrow GF \end{align*} and counit \begin{align*} \varepsilon: FG \Rightarrow \operatorname{id}_{\mathcal D}, \end{align*} and assume that both natural transformations are natural isomorphisms. To exhibit an equivalence of categories, we need functors $F: \mathcal C \to \mathcal D$ and $G: \mathcal D \to \mathcal C$ together with natural isomorphisms from $\operatorname{id}_{\mathcal C}$ to $GF$ and from $FG$ to $\operatorname{id}_{\mathcal D}$. The functors are the given functors, the first natural isomorphism is $\eta$, and the second natural isomorphism is $\varepsilon$. Therefore $G$ is a quasi-inverse to $F$, and $F$ and $G$ form an equivalence of categories.[/guided]