Vaughan Pratt wrote:
... The Yoneda Lemma usually states that J embeds (meaning fully) in [J^op,Set], ...
Dear Vaughan, The usual statement is significantly stronger than that (see e.g. Mac Lane, Mac Lane and Moerdijk, or Wikipedia). It says that, for contravariant functors F: C -> Set, the elements of FX are in bijection with transformations to F from the representable functor for X. Your statement can be deduced by considering the particular case where F too is representable. (To put it another way, the representable presheaf for X is freely generated - as presheaf - by a single element (the identity morphism) at X. This then allows you to calculate the left adjoint of the forgetful functor from presheaves over C to ob(C)-indexed families of sets.) There can be no doubt that this strong Yoneda Lemma is vitally important when calculating with presheaves - for example, it shows immediately how to calculate exponentials and powerobjects. If F and G are two presheaves, then the exponential G^F is calculated by G^F(X) = nt(Y(X), G^F) (by Yoneda's Lemma) = nt(Y(X) x F, G) (by definition of exponential) I don't think you can get it and its useful consequences from your weaker statement, even if you start strengthening yours in the way you suggest by supplying converses. Another closely related and important result, though not known as Yoneda's Lemma as far as I know, is that the presheaf category over C is a free cocompletion of C, and the Yoneda embedding is the injection of generators. (By the way, I agree that category theory doesn't have to have a Fundamental Theorem. I haven't see any compelling reason to appoint one.) Regards, Steve. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]