The definition of adjoint functors is straightforward; the main interesting aspect arises from proof-relevance.

###### Definition 9.3.1.

A functor $F:A\to B$ is a left adjoint if there exists

• A functor $G:B\to A$.

• $\eta:1_{A}\to GF$ (the unit).

• A natural transformation $\epsilon:FG\to 1_{B}$ (the counit).

• $(\epsilon F)(F\eta)=1_{F}$.

• $(G\epsilon)(\eta G)=1_{G}$.

The last two equations are called the triangle identities or zigzag identities. We leave it to the reader to define right adjoints analogously.

###### Lemma 9.3.2.

If $A$ is a category (but $B$ may be only a precategory), then the type “$F$ is a left adjoint” is a mere proposition.

###### Proof.

Suppose we are given $(G,\eta,\epsilon)$ with the triangle identities and also $(G^{\prime},\eta^{\prime},\epsilon^{\prime})$. Define $\gamma:G\to G^{\prime}$ to be $(G^{\prime}\epsilon)(\eta^{\prime}G)$, and $\delta:G^{\prime}\to G$ to be $(G\epsilon^{\prime})(\eta G^{\prime})$. Then

 $\displaystyle\delta\gamma$ $\displaystyle=(G\epsilon^{\prime})(\eta G^{\prime})(G^{\prime}\epsilon)(\eta^{% \prime}G)$ $\displaystyle=(G\epsilon^{\prime})(GFG^{\prime}\epsilon)(\eta G^{\prime}FG)(% \eta^{\prime}G)$ $\displaystyle=(G\epsilon)(G\epsilon^{\prime}FG)(GF\eta^{\prime}G)(\eta G)$ $\displaystyle=(G\epsilon)(\eta G)$ $\displaystyle=1_{G}$

using \autorefct:interchange and the triangle identities. Similarly, we show $\gamma\delta=1_{G^{\prime}}$, so $\gamma$ is a natural isomorphism $G\cong G^{\prime}$. By \autorefct:functor-cat, we have an identity $G=G^{\prime}$.

Now we need to know that when $\eta$ and $\epsilon$ are transported along this identity, they become equal to $\eta^{\prime}$ and $\epsilon^{\prime}$. By \autorefct:idtoiso-trans, this transport is given by composing with $\gamma$ or $\delta$ as appropriate. For $\eta$, this yields

 $(G^{\prime}\epsilon F)(\eta^{\prime}GF)\eta=(G^{\prime}\epsilon F)(G^{\prime}F% \eta)\eta^{\prime}=\eta^{\prime}$

using \autorefct:interchange and the triangle identity. The case of $\epsilon$ is similar. Finally, the triangle identities transport correctly automatically, since hom-sets are sets. ∎

In \autorefsec:yoneda we will give another proof of \autorefct:adjprop.