Which satisfy the triangle identities (a.k.a zig-zag identities)

$(\epsilon F)(F \eta) = 1_F$

$(G \epsilon)(\eta G) = 1_G$

Properties

Lemma 9.3.2

If $A$ s a category and $B$ is 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', \eta', \epsilon')$. Define $\gamma: G \to G'$ to be $(G' \epsilon )(\eta G')$. Then

$\begin{aligned}
\delta \gamma &= (G \epsilon')(\eta G')(G' \epsilon) (\eta' G)\\
&= (G \epsilon')(G F G' \epsilon_))\eta G' F G)(\eta' G)\\
&= (G \epsilon ')(G \epsilon' F G)(G F \eta' G)(\eta G)\\
&= (G \epsilon)(\eta G)\\
&= 1_G
\end{aligned}$