The definition of adjoint functors is straightforward; the main interesting aspect arises from proof-relevance.
The last two equations are called the triangle identities or zigzag identities. We leave it to the reader to define right adjoints analogously.
Suppose we are given with the triangle identities and also . Define to be , and to be . Then
using \autorefct:interchange and the triangle identities. Similarly, we show , so is a natural isomorphism . By \autorefct:functor-cat, we have an identity .
Now we need to know that when and are transported along this identity, they become equal to and . By \autorefct:idtoiso-trans, this transport is given by composing with or as appropriate. For , this yields
using \autorefct:interchange and the triangle identity. The case of 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.