no offense, steve, but we are for some reason telling each other things that we both surely know that we both know them.

The composite morphism

(all) x.P(x) --> P(a) --> (exists) x.P(x)

exists only when we have a in A.

internally, of course, every A thinks that there is an a in A. that is what its free variable of type A tells it. when A=0, then the predicate P(a), for free a, as well as the inverse images of (all) x.P(x) and of (exists) x.P(x) along the map 0-->1, all boil down to the same predicate 0-->Prop. so they turn out to be quite equivalent.

Second, in your proof with contexts, you use "the equivalence true |-() ((all) b. ((all) a. P(a) --> (exists) x. P(x))) <-> (((all) a. P(a) --> (exists) x. P(x)))" You didn't give a proof of this equivalence,

because i thought that some people would remember that it is just the good old Beck-Benabou-Chevalley-Roubaud condition (to list the discoverers alphabetically); whereas the others would be satisfied that quantifying over a variable b, that does not occur in a predicate, does not change the truth value of that predicate. but i do see what you are saying when we take P:0-->Prop to be a 0-indexed family of propositions, and interpret the quantifiers as the meet and the join: the empty meet is indeed greater than the empty join. so the logicians are eliminating the empty domain in order to avoid having to specify the inverse images. (i think i used to know that.) isn't it unreasonable to sacrifice a part of the structure (a fairly ubiquitous object) to a mere syntactic habit? i thought categorical logic had provided a good solution to the "nonempty domain" nuisance from the 50s logic books. all the best (and i really have to work now), -- dusko [For admin and other information see: http://www.mta.ca/~cat-dist/ ]