Homotopy Type Theory
left adjoint


Many naturally arising functors in mathematics have adjoints. This makes them a useful thing to study.


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

  • A functor G:BAG : B \to A
  • A natural transformation η:1 AGF\eta:1_A \to G F (the unit).
  • A natural transformation ϵG1 B\epsilon G \to 1_B (the counit).
  • Which satisfy the triangle identities (a.k.a zig-zag identities)
    • (ϵF)(Fη)=1 F(\epsilon F)(F \eta) = 1_F
    • (Gϵ)(ηG)=1 G(G \epsilon)(\eta G) = 1_G


Lemma 9.3.2

If AA s a category and BB is a precategory then the type “FF is a left adjoint” is a mere proposition?.

Proof. Suppose we are given (G,η,ϵ)(G, \eta, \epsilon) with the triangle identities and also (G,η,ϵ)(G', \eta', \epsilon'). Define γ:GG\gamma: G \to G' to be (Gϵ)(ηG)(G' \epsilon )(\eta G'). Then

δγ =(Gϵ)(ηG)(Gϵ)(ηG) =(Gϵ)(GFGϵ ))ηGFG)(ηG) =(Gϵ)(GϵFG)(GFηG)(ηG) =(Gϵ)(ηG) =1 G \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}

using Lemma 9.2.8 (see natural transformation) and the triangle identities. Similarly, we show γδ=1 G\gamma \delta=1_{G'}, so γ\gamma is a natural isomorphism GGG \cong G'. By Theorem 9.2.5 (see functor precategory), we have an identity G=GG=G'.

Now we need to know that when η\eta and ϵ\epsilon are [transported]] along this identity, they become equal to η\eta' and ϵ\epsilon '. By Lemma 9.1.9,

Lemma 9.1.9 needs to be included. For now as transports are not yet written up I didn’t bother including a reference to the page category. -Ali

this transport is given by composing with γ\gamma or δ\delta as appropriate. For η\eta, this yields

(GϵF)(ηGF)η=(GϵF)(GFη)η=η(G' \epsilon F)(\eta' G F)\eta = (G' \epsilon F)(G' F \eta)\eta'=\eta'

using Lemma 9.2.8 (see natural transformation) and the traingle identity. The case of ϵ\epsilon is similar. FInally, the triangle identities transport correctly automatically, since hom-sets are sets. \square

See also

Category theory


natural transformation


HoTT Book

category: category theory

Last revised on October 11, 2018 at 06:32:21. See the history of this page for a list of all contributions to it.