I guess simplicity is in the eye of the beholder. For example, I do not consider the categorical version of either choice (epis split) or well-pointed (1 is a generator) to be translations of set theory, but perfectly natural categorical axioms. The point is that Harvey is a set-theorist, so he thinks comprehension and all that stuff (which at least 95% of all mathematicians could not state properly if their lives depended on it) is perfectly natural and I don't. But my actual criticism of ZF(C) is much simpler. I have taught these courses in set theory and we spend a lot of time developing these epsilon trees and then totally ignore the structure. In other words, the epsilon tree structure of sets is totally irrelevant to what you do with them. There are a number of definitions of pairs, but they are irrelevant. The only thing we need to know about pairs (and the only thing a categoriest does know) is when two pairs are equal. All the defintions of pairs have that property of course, but they also have irrelevant properties. Mike