Here are some remarks on Duskos reaction on my comments about comprehension. What I meant was the following : comprehension is a means for TRANSFORMING PROPOSITIONS (i.e. objects in the fibre of some hyperdoctrine) to DATATYPES (i.e. objects in the base) in other words it allows to CONSIDER collections of proofs as types of objects. That is what I would call a mixing of levels of language : "data" are "real objects" WHEREAS "proofs" are "meta objects" . So one might be able to define functions which depend on proof objects but deliver say natural numbers. If I remember correctly exactly this is what Dusko wants to avoid by his theory of predicates. Thomas Streicher P.S. I - of course - do not mean that comprehension is "inconsistent" BUT I mean that it changes the notion of algorithm considerably and in an unintuitive way.