9.3 Adjunctions

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

Definition 9.3.1.

A functorMathworldPlanetmath F:AB is a left adjoint if there exists

  • A functor G:BA.

  • A natural transformation η:1AGF (the unit).

  • A natural transformation ϵ:FG1B (the counit).

  • (ϵF)(Fη)=1F.

  • (Gϵ)(ηG)=1G.

The last two equations are called the triangle identities or zigzag identitiesPlanetmathPlanetmath. 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.


Suppose we are given (G,η,ϵ) with the triangle identities and also (G,η,ϵ). Define γ:GG to be (Gϵ)(ηG), and δ:GG to be (Gϵ)(ηG). Then

δγ =(Gϵ)(ηG)(Gϵ)(ηG)

using \autorefct:interchange and the triangle identities. Similarly, we show γδ=1G, so γ is a natural isomorphism GG. By \autorefct:functor-cat, we have an identity G=G.

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.

Title 9.3 Adjunctions