background to my question

18 Jan 1992

      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
======================================