9.5 The Yoneda lemma

Recall that we have a categoryMathworldPlanetmath 𝒮et whose objects are sets and whose morphismsMathworldPlanetmath are functions. We now show that every precategory has a 𝒮et-valued hom-functor. First we need to define opposites and productsPlanetmathPlanetmathPlanetmathPlanetmath of (pre)categories.

Definition 9.5.1.

For a precategory A, its opposite Aop is a precategory with the same type of objects, with homAop(a,b):homA(b,a), and with identities and composition inherited from A.

Definition 9.5.2.

For precategories A and B, their product A×B is a precategory with (A×B)0:A0×B0 and


Identities are defined by 1(a,b):(1a,1b) and composition by (g,g)(f,f):((gf),(gf)).

Lemma 9.5.3.

For precategories A,B,C, the following types are equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath.

  1. 1.

    FunctorsMathworldPlanetmath A×BC.

  2. 2.

    Functors ACB.


Given F:A×BC, for any a:A we obviously have a functor Fa:BC. This gives a function A0(CB)0. Next, for any f:homA(a,a), we have for any b:B the morphism F(a,b),(a,b)(f,1b):Fa(b)Fa(b). These are the componentsPlanetmathPlanetmath of a natural transformation FaFa. Functoriality in a is easy to check, so we have a functor F^:ACB.

Conversely, suppose given G:ACB. Then for any a:A and b:B we have the object G(a)(b):C, giving a function A0×B0C0. And for f:homA(a,a) and g:homB(b,b), we have the morphism


in homC(G(a)(b),G(a)(b)). Functoriality is again easy to check, so we have a functor Gˇ:A×BC.

Finally, it is also clear that these operationsMathworldPlanetmath are inversesPlanetmathPlanetmathPlanetmath. ∎

Now for any precategory A, we have a hom-functor


It takes a pair (a,b):(Aop)0×A0A0×A0 to the set homA(a,b). For a morphism (f,f):homAop×A((a,b),(a,b)), by definition we have f:homA(a,a) and f:homA(b,b), so we can define

(homA)(a,b),(a,b)(f,f) :(g(fgf))

Functoriality is easy to check.

By \autorefct:functorexpadj, therefore, we have an induced functor 𝐲:A𝒮etAop, which we call the Yoneda embedding.

Theorem 9.5.4 (The Yoneda lemma).

For any precategory A, any a:A, and any functor F:SetAop, we have an isomorphismMathworldPlanetmathPlanetmathPlanetmathPlanetmath

hom𝒮etAop(𝐲a,F)Fa. (9.5.4)

Moreover, this is natural in both a and F.


Given a natural transformation α:𝐲aF, we can consider the component αa:𝐲a(a)Fa. Since 𝐲a(a)homA(a,a), we have 1a:𝐲a(a), so that αa(1a):Fa. This gives a function (ααa(1a)) from left to right in (9.5.4).

In the other direction, given x:Fa, we define α:𝐲aF by


Naturality is easy to check, so this gives a function from right to left in (9.5.4).

To show that these are inverses, first suppose given x:Fa. Then with α defined as above, we have αa(1a)=Fa,a(1a)(x)=1Fa(x)=x. On the other hand, if we suppose given α:𝐲aF and define x as above, then for any f:homA(a,a) we have

αa(f) =αa(𝐲aa,a(f))

Thus, both composites are equal to identities. We leave the proof of naturality to the reader. ∎

Corollary 9.5.6.

The Yoneda embedding y:ASetAop is fully faithful.


By \autorefct:yoneda, we have


It is easy to check that this isomorphism is in fact the action of 𝐲 on hom-sets. ∎

Corollary 9.5.7.

If A is a category, then y0:A0(SetAop)0 is an embeddingMathworldPlanetmath. In particular, if ya=yb, then a=b.


By \autorefct:yoneda-embedding, 𝐲 induces an isomorphism on sets of isomorphisms. But as A and 𝒮etAop are categories and 𝐲 is a functor, this is equivalently an isomorphism on identity types, which is the definition of being an embedding. ∎

Definition 9.5.8.

A functor F:SetAop is said to be representable if there exists a:A and an isomorphism yaF.

Theorem 9.5.9.

If A is a category, then the type “F is representable” is a mere proposition.


By definition “F is representable” is just the fiber of 𝐲0 over F. Since 𝐲0 is an embedding by \autorefct:yoneda-mono, this fiber is a mere proposition. ∎

In particular, in a category, any two representations of the same functor are equal. We can use this to give a different proof of \autorefct:adjprop. First we give a characterization of adjunctionsPlanetmathPlanetmath in terms of representability.

Lemma 9.5.10.

For any precategories A and B and a functor F:AB, the following types are equivalent.

  1. 1.

    F is a left adjoint.

  2. 2.

    For each b:B, the functor (ahomB(Fa,b)) from Aop to 𝒮et is representable.


An element of the type 2 consists of a function G0:B0A0 together with, for every a:A and b:B an isomorphism


such that γa,b(gFf)=γa,b(g)f for f:homA(a,a).

Given this, for a:A we define ηa:γa,Fa(1Fa), and for b:B we define ϵb:(γGb,b)-1(1Gb). Now for g:homB(b,b) we define


The verifications that G is a functor and η and ϵ are natural transformations satisfying the triangle identities are exactly as in the classical case, and as they are all mere propositions we will not care about their values. Thus, we have a function 21.

In the other direction, if F is a left adjoint, we of course have G0 specified, and we can take γa,b to be the composite


This is clearly natural since η is, and it has an inverse given by


(by the triangle identities). Thus we also have 1 2.

For the composite 21 2, clearly the function G0 is preserved, so it suffices to check that we get back γ. But the new γ is defined to take f:homB(Fa,b) to

G(f)ηa γGFa,b(fϵFa)ηa

so it agrees with the old one.

Finally, for 12 1, we certainly get back the functor G on objects. The new Gb,b:homB(b,b)homA(Gb,Gb) is defined to take g to

γGb,b(gϵb) G(gϵb)ηGb

so it agrees with the old one. The new ηa is defined to be γa,Fa(1Fa)G(1Fa)ηa, so it equals the old ηa. And finally, the new ϵb is defined to be (γGb,b)-1(1Gb)ϵbF(1Gb), which also equals the old ϵb. ∎

Corollary 9.5.11.

[\autorefct:adjprop] If A is a category and F:AB, then the type “F is a left adjoint” is a mere proposition.


By \autorefct:representable-prop, if A is a category then the type in \autorefct:adj-repr2 is a mere proposition. ∎

Title 9.5 The Yoneda lemma