I think it might be interesting for some people to get explained the background of the question I posed on the e-mail forum and which has been ANSWERED by P. FREYD in a very pleasing and hepful way. Some time ago I was asking myself two questions. In the situation that one is given an lccc C and a class of display maps D respresenting a full internally complete category of C : 1) does this imply that display maps are closed under composition, i.e one has strong sums for this question the answer is no and described in my MSCS paper "Dependence and Independence Results for (Impredicative) Type Theories " 2) if one assumes that there is a generic morphism for D then by an internalization of FAFT one can prove that the full subcat as given by D is reflective in the fibrational sense, i.e. one has weak sums or existential quantification now the question was whether existential quantification is still guaranteed if one drops the assumption that there exists a generic morphism, i.e. the assumption of SMALLness the answer to this last question is NO and the counterexample - BASED on Peter FREYDs helpful lemma - is the following : take an lccc C together with a class of display maps D representing a full internally complete subcat of C ; let N* be the category which is the opposite of natural numbers extended with an object inf strictly greater than all natural numbers n ; now N* x C is an lccc , too, but now take as display maps those morphisms (x -> y , f ) : (x,A) -> (y,I) where f : A -> I is in D and x = inf iff y = inf ; let us call this new class of display maps DN ; then for the lccc N* x C with this new class DN of diplay maps it is the case that DN represents a full internally complete subcat of N* x C BUT it is NOT reflective !! Another question arising in this context is : How is the whole question related to sub-lccc-ness of the category represented by D ?? We call D REPRESENTING a FULL SUB-LCC of C iff for any object I of C the full subcat D / I of C / I is a full sub-lccc . What I have shown in my MSCS paper is that If D represent a full sub-lccc of C then D is closed under composition !! On the other hand if D represents a full internally complete subcat of C and D is closed under composition then D represents a full sub-lcc of C . What I also have shown in my MSCS paper is that If you take for C the category w-Set and for D those morphisms corresponding to families of extensional pers then D is NOT closed under composition, thus it does not represent a full sub-lccc ! This, of course, does not immediately imply that the category of extensional pers is not lccc . BUT my counterexample contains more. I have constructed a morphism f : Y -> X where Y and X are extensional pers and such that it holds that the domain of Pi (! X) f is not isomorphic to an extensional per . Thus extensional pers do not form a sub-lccc of w-Set ! Even more one can show that X is Sigma replete and f represents a family of Sigma replete pers. Let us call Y.x the family of pers corresponding to f . Of course, there is more to be shown than that for any x in X the Y.x is Sigma replete ! (Thanks to Wesley Phoa for pointing me to this problem !) But as Y.x is [Z.x -> Sigma] for a family Z.x of pers , one can realize UNIFORMLY IN x that Y_x is Sigma replete ! Thus w.r.t. the following aspects in Synthetic Domain Theory the situation is the same as in ordinary domain theory : The category of predomains is complete, but not lccc ! Thomas Streicher ======================================