Dear Community, I am recently racking my brains in trying to understand what (im-)predicativity means from a categorical perspective, but failing short, hence calling for you help. Certain constructive principle are easy to accommodate (and understand!) within category theory, e.g. the axiom of choice (all epis are split), excluded middle (every mono is a coproduct summand), however this does not seem to be the case with the notion of predicativity. The rough intuition says that impredicative definitions attempt to define things topdown: first by introducing a class, and then defining elements of this class by their characteristic properties -- arguably, a controversial idea, if you strive for foundations. That intuition is sort of helpful to deal with extreme cases, e.g. to accept that toposes are impredicative, and Martin-L??f type theory is predicative, but it does not seem to give a complete answer. The discussion and the papers I found on the web rather seem to reflect the set-theoretic tradition in categorical terms, than to explain the issue intrinsically. Let me clarify. We agree that toposes are impredicative (or, at least not compatible with predicative approach) because they include subobject classifiers, and those arguably classify to much, for according to Bishop, we have no idea a priory, what an arbitrary subset of given set is like. On the other hand, classifying *something* can be OK, e.g. in extensive categories we can classify summands: 2 = 1 + 1 is a summand classifier, and extensive categories are certainly not considered to be impredicative, for every pretopos is extensive. Now, there is a spectrum of classes of monomorphisms that could be classified, depending on a category. I could e.g. try to classify r.e-subsets in an effective topos. How can I know, if it is still OK or not OK from a predicative perspective? (I realize that if we reject impredicativity in foundations, we probably just can not construct any example of a topos, including the effective one, but suppose, I still can make sense of this idea of classifying r.e.-subsets somehow without constructing a topos). Sorry, if that all sounded jumbled, but maybe you can understand my concerns. I presume that a complete answer just does not exist, and would be a subject to an open research, but I would be happy to understand at least informally what sort of justification is used to claim that one category is predicative (or predicative-friendly) and another one is not. Looking forward to your answers. Sergey [For admin and other information see: http://www.mta.ca/~cat-dist/ ]