Thanks again. Due to this observation by choosing for A the categories Set , omega-Set or PER-omega we get counterexamples which are very rich. IsnBt it the case that by taking the product of some lccc A with e.g. the nat ural numbers with inverse order one gets some aspect of "time" into realizabili ty models which destroy the existence of existential quantifiers. Maybe it is worthwhile to investigate connections with Martin-LoefBs work in mathematics of infinity where he considers sequences of models of type theory in order to explain infinite objects. Thomas Streicher P.S. I think a further interesting counterexample is obtained by taking for C the product of 0mega-Set with (N u {infinity})* and for D the full subcatego ry which is the cartesian product of PER-omega with (N u {infinity})*. ======================================