Dear all, As Thomas and Bill pointed out, the effective topos is quite far from being cocomplete; indeed, a countable coproduct of copies of 1 does not exist. So the locally finitely presentable machinery seems not to work here, at least, externally. Bill points to Mulry's recursive topos as an approximation. Here is a question, related to a possible other approximation. Does the effective topos have a dense set of generators? In this case one could embed it into a Grothendieck topos by an embedding which preserves a lot of structure. It is easy to see that the full subcategory of Eff on the countable projective objects is essentially small and generates Eff. But is it dense? This is related to the following question: does the functor Nabla: Sets --> Eff preserve \omega _1-filtered colimits? (it is easy to see that it doesn't preserve filtered colimits; it does preserve \omega _1-filtered colimits as functor from Sets to the separated objects of Eff) I have been trying for some time to solve this; but I couldn't. It appears that set-theoretic combinatorics plays an important role here, and is more important than recursiveness. Jaap van Oosten 11-Jan-2002 08:51:05 -0400,2228;000000000000-00000000