I certainly welcome Ross' clarification of his problem. One possibility would be to give the proof except for the existence of sufficient regular functors and either refer the students to the paper or (better) write it out carefully and distribute it. One thing I have given only a little thought to is whether it can be done using a maximal principle argument. The point is that it is not a question of extending a map to a larger and larger subobject, but of building larger and larger objects and not as subobjects of something already given. This makes it different from the proof, say, that divisible abelian groups are injective (from which the existence of sufficient injectives in any module category follows easily). I think a maximal principle argument goes down a lot more easily than one based overtly on ordinals or transfinite induction. Ross, it sounds like a beautiful course and if you have notes, I would like to see them. Michael