In reply to Steve Vickers' post, I have a few comments. First off, it was not Lubkin-Heron-Freyd-Mitchell who proved the full embedding theorem. The first three proved only a faithful functor into set (and subject to some smallness condition), while Mitchell showed the full embedding theorem. And not merely into a Grothendieck abelian category, but one with a small projective generator. The analogue would be an embedding into a set-valued functor category. Unfortunately, a beautiful observation of Makkai's shows that that is impossible. Makkai pointed out that under a full embedding that preserves finite limits, finite sums and epis the boolean algebra of complemented subobjects, which is classified by maps into 1 + 1, would have to be preserved. But in a functor category that lattice is complete and atomic (that is, completely distributive), so that fact, which is not true for toposes in general, becomes a necessary condition for the existence of an embedding. (Is it sufficient?) There is, of course, a full embedding theorem for small exact categories, but that is a lot less than a topos. But is true that additive + exact = abelian, so maybe that is also a good analogy. Michael