Actually to my opinion we do not need the full topos logic it is sufficient to consider triposes. I think the axiom of comprehension : A type , P predicate on A --------------------------------- { x : A | P(x) } type is not very nice to work with syntactically. I appreciate Thomas Streicher's interesting observation about PERs but I don't see how does it lead him to this opinion about the comprehension. Comprehension is not a special property of PERs, nor are PERs its special model. Comprehension doesn't seem to play any role here. PERs are used as propositions/truth values when one uses them to model something like the Theory of Constructions. (Comprehension comes in, I suppose, only in a paper where I showed that Constructions can be given a familiar "set-theoretical" appearance, Springer LNCS #530.) I do not understand the point of comparing whether it is better to use Constructions (with or without comprehension) or the internal language of a topos. These things are at different levels. (Tripos is clearly weaker. For some purposes, however, I am sure that even first order logic will do.) Regards to all, Dusko Pavlovic P.S. Concerning the proof-theoretical difficulties with comprehension (if this is meant by "not very nice to work with") I can only say that these difficulties can not be a sufficient reason to dismiss a logical operation. Comprehension is certainly less difficult than the sum or the existential quantifier. ======================================