Yoneda on a not so small category I am working with "usual" category theory, maybe over ZFC, and I have a functor $F : Set \to Set$. I'd like to apply Yoneda lemma to $F$, i.e. obtain:
$$ [Set, Set](h_A, F) \cong F A $$
However, most of texts assume that the domain of $F$ should be a small category in order to apply it. I know this has to do with the size of $[Set, Set]$ and the existence of $h_A$. How could I fix my foundations so I can use Yoneda lemma like this? Or I'll never be able to do such thing?
 A: You could use the usual device of assuming a Grothendieck universe: Mac Lane does this in [Categories for the working mathematician]. But actually you don't need that for the Yoneda lemma – you could just rephrase things so that there is no mention of the "illegal" category $[\mathbf{Set}, \mathbf{Set}]$. For instance:

For any functor $F : \mathbf{Set} \to \mathbf{Set}$, any set $A$, and any element $x$ of $F(A)$, there is a unique natural transformation $\theta_x : \mathbf{Set}(A, -) \Rightarrow F$ such that $(\theta_x)_A (\mathrm{id}_A) = x$.

Of course, logicians will point out that the above is really a "metatheorem" because functors $\mathbf{Set} \to \mathbf{Set}$ are not elements of the universe of discourse, but that's not really important. (Since you mention it, the "existence" of $\mathbf{Set}(A, -)$ is never a problem: it may not be an element of the universe, but what it does is perfectly well-defined.) One can avoid this particular issue of metatheorem vs theorem by switching from ZFC to NBG, but if you prefer to avoid having to think about fine distinctions like that at all, you should just bite the bullet and use a Grothendieck universe. (My preference nowadays is to assume a Grothendieck universe inside Mac Lane set theory.)
A: The problem is not whether you can use Yoneda lemma or not, but to associate a precise meaning to your sentences. As a rule of thumb, Yoneda lemma works whenever you can formally say what it actually means.
I do not agree with Zhen's answer which says that it is not really important that the objects are not inside the universe --- the truth is exactly the opposite --- it is the only issue here. In the usual ZFC formalization, objects $FA$ are real sets, whereas objects $\mathit{nat}(h_A, F)$ are not. Of course you can "lift" $FA$ to the meta-universe, but then you will compare apples with apes.
A: Zhen Lin states one direction of the Yoneda Lemma: given $x\in F A$, the natural transformation $\theta_x:H_A\to F$ on $f:A\to B$ is $\theta(f)=F f\cdot x$.  The other direction is that every $\theta:H_A\to F$ is of this form, where $x=\theta(\mathsf{id}_A)$. I leave it as an exercise to show that $\theta_x$ is natural and that this correspondence is bijective.
What I have just stated is the natural mathematical argument for the central idea of the Yoneda Lemma, albeit without the calculations required for the proofs. None of it has anything to do with Set Theory, whether that be ZFC, NBG or even NF.
This argument makes sense in a world in which objects and morphisms are things of a different sort from one another. Functors and natural transformations, on the other hand, are schemes or recipes that transform objects and morphisms into objects and morphisms. Functors and natural transformations are not themselves things.
We are quite used to this many-sorted language in algebra or first order logic. Even when the algebra itself has only one sort (if you don't know what I mean by that, I mean exactly the situation that you know), elements of the algebra, homomorphisms, predicates, ideals etc. belong to different sorts of the language in which we discuss them.
It was the innovation of Set Theory to reify schemes, i.e. turn them into things. In its unrestricted form, this innovation led to the famous antinomies or paradoxes, such as Russell's.  The outcome of this was to develop restricted reification, such as Zermelo Set Theory.
Unfortunately, the mathematical community became addicted to Cantor's "paradise". So, even in disciplines such as Category Theory where we should have known better, we continue to find attempts at unrestricted reification such as Grothendieck Universes.
The disciplined alternative is the type-theoretic style, in which we nominate certain forms of reification, for example that of functions ($\lambda$-abstraction), and stick to just those (in the context of a particular discourse).
Now to reply to Michal Przybylek.  I have just said and he agrees that "If people think that they need any kind of Set Theory to speak about Yoneda lemma, then they are wrong." However, far from being "philosophical" or "waving my hands", I have explained quite precisely what is the methodological set-up ("foundations" if you wish) behind the argument.
At least, I discussed the ordinary form of the argument.  Of course, as mathematicians have always done extremely profitably with pre-existing arguments, one may re-interpret it in more exotic settings. Enriched, internal and locally cartesian closed categories are examples of such settings.  Moreover they are also examples of desciplined restricted reification operations.
