9.3 Adjunctions
The definition of adjoint functors^{} is straightforward; the main interesting aspect arises from proofrelevance.
Definition 9.3.1.
A functor^{} $F\mathrm{:}A\mathrm{\to}B$ is a left adjoint if there exists

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

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

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

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

•
$(G\u03f5)(\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 ,\u03f5)$ with the triangle identities and also $({G}^{\prime},{\eta}^{\prime},{\u03f5}^{\prime})$. Define $\gamma :G\to {G}^{\prime}$ to be $({G}^{\prime}\u03f5)({\eta}^{\prime}G)$, and $\delta :{G}^{\prime}\to G$ to be $(G{\u03f5}^{\prime})(\eta {G}^{\prime})$. Then
$\delta \gamma $  $=(G{\u03f5}^{\prime})(\eta {G}^{\prime})({G}^{\prime}\u03f5)({\eta}^{\prime}G)$  
$=(G{\u03f5}^{\prime})(GF{G}^{\prime}\u03f5)(\eta {G}^{\prime}FG)({\eta}^{\prime}G)$  
$=(G\u03f5)(G{\u03f5}^{\prime}FG)(GF{\eta}^{\prime}G)(\eta G)$  
$=(G\u03f5)(\eta G)$  
$={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:functorcat, we have an identity $G={G}^{\prime}$.
Now we need to know that when $\eta $ and $\u03f5$ are transported along this identity, they become equal to ${\eta}^{\prime}$ and ${\u03f5}^{\prime}$. By \autorefct:idtoisotrans, this transport is given by composing with $\gamma $ or $\delta $ as appropriate. For $\eta $, this yields
$$({G}^{\prime}\u03f5F)({\eta}^{\prime}GF)\eta =({G}^{\prime}\u03f5F)({G}^{\prime}F\eta ){\eta}^{\prime}={\eta}^{\prime}$$ 
using \autorefct:interchange and the triangle identity. The case of $\u03f5$ is similar. Finally, the triangle identities transport correctly automatically, since homsets are sets. ∎
In \autorefsec:yoneda we will give another proof of \autorefct:adjprop.
Title  9.3 Adjunctions 

\metatable 