On Fri, 7 Feb 2003 jvoosten@math.uu.nl wrote:
I think the relevance of this condition (Sxy defined) is explained in the Hyland-Ong paper "Modified Realizability Toposes and Strong Normalization Proofs" (TLCA, LNCS 664, 1993; reference 466 in the Elephant) where they have a definition of "c-pca" which is just omitting this requirement. They show that the standard P(A)-indexed preordered set, for a c-pca A, can fail to be a tripos. So the condition IS used.
I hope Jaap and Peter will forgive me for saying that I think they missed the point of my message. (Perhaps it's my fault -- with hindsight, I wasn't as clear as I should have been. I really ought to stop trying to reply to things like this late at night -- although, as you'll see from the header of this message, I'm doing it again.) Of course I know about the Hyland--Ong paper: indeed, I reviewed it for Zentralblatt. However, the point I was trying to make was that the construction of the quasitopos of A-valued assemblies, and the proof that its effectivization is a topos, make no use whatever of the condition that Sxy is always defined. The fact that the tautology ((p => (q => r)) => ((p => q) => (p => r))) fails (or may fail) to be realized by S when p is empty has no effect on this construction, because one never has to deal with "propositions" having an empty set of realizers. So, whilst a tripos-theorist (if such a creature exists) may indeed have cause to worry about whether Sxy might be undefined, there seems to be no reason why a topos-theorist should do so. [Yes, yes, I know that I was responsible for inventing the term "tripos", and therefore that if anyone can legitimately be called a tripos-theorist then I can. But I don't believe that I am a tripos-theorist (which implies that no-one is).] Peter Johnstone