Dear John, would you please fill me in on either (or better yet, both) of the following points, as I failed to figure them out by myself: 1.) Let A be a c-pca. If I understand correctly, you say that the indexed poset that maps a set I to the set of maps from I to P(A), endowed with the usual entailment relation [ for phi,psi: I -> P(A), phi |- psi iff there is an r in A such that for all i in I and for all a in phi(i), ra exists and ra is in psi(i) ] is indeed an indexed Heyting-Algebra and that the implication of phi,psi : I -> P(A) is given by (phi=>psi)(i) = {r in A | forall a in phi(i). rka in psi(i)}. My question is: given phi, psi and theta such that theta /\ phi |- psi over I via some realizer r, what would be a realizer witnessing theta |- phi => psi with => defined in the way you indicated? 2.) Given a c-pca A, you say that A equipped with the application function a.b := akb is a (proper) pca. What exactly would be a good S combinator for the new algebra ? (You wrote that some additional care is needed to construct S) Many thanks in advance, Peter ps: in an attempt to give the shortest possible of the many reasons, why Heyting algebras do not form a CCC I suggest: The one-element poset is the terminal Heyting algebra. Therefore, every object has at most one global section. Hence, there can only be one morphism between each two Heyting algebras, as the global sections of the exponent correspond to the morphisms (which is absurd). pps: The one-element poset *is* a Heyting-algebra, in fact all topologies are. On Wed, 12 Feb 2003, John Longley wrote:
As far as I can see, Peter Johnstone is essentially correct. Even without the condition "sxy is defined", Asm(A) is locally cartesian closed (though the correct construction of local exponentials is not quite the "obvious" one), and its exact/regular completion is a topos. Peter Lietz's argument (which is the one that occurred to me too) seems to fail at his point 1: to get a realizer for the mediating morphism from the true local exponential to the object he constructs, one actually needs the condition "sxy is defined". For the record, in Peter L's example, the true exponential m^m in the slice over Nabla(P(A)), for instance,
....