Subject:     full internally complete sub-lccc-s
Date: Fri, 14 Dec 90 11:37:25 +0100
From: streiche@unipas.fmi.uni-passau.de (Thomas Streicher)


  I am interested in the following question. Given any lccc (locally cartesian
closed category) C  can one find a full internally complete sub-category which
is NOT reflective ?  Of course, I mean subcategory in the fibrational sense !

The answer is well known in the case that the subcategory is SMALL !
Then by FAFT internal completeness is equivalent to reflectiveness.

My guess is that for full subcategories of an lccc (in the fibrational sense)
the property of having equalizers fibrewise being stable under reindexing is
NOT equivalent to smallness !

But what I am lacking is a counterexample. I have tried the Freyd cover of
'w'-Set (the category of realizability sets) but unfortunately this construct-
ion preserves those colimits I wanted to get rid of.

I also would be quite satisfied with a counterexample in the non-fibred case.
But I guess in the category of sets such a counterexample cannot be found.


                                                          Thomas Streicher

Subject:     Re:  full internally complete sub-lccc-s
Date: Mon, 17 Dec 90 15:52:22 EST
From: pjf@saul.cis.upenn.edu (Peter Freyd)
Subject: Re:  full internally complete sub-lccc-s

Thomas Streicher asks:

  I am interested in the following question. Given any lccc (locally cartesian
closed category) C  can one find a full internally complete sub-category which
is NOT reflective ? ...
I also would be quite satisfied with a counterexample in the non-fibred case.
But I guess in the category of sets such a counterexample cannot be found.

I reply:

Are you sure this is the right question?  Consider the dual of the order-type
of the ordinal numbers.  View it as a category and formally adjoin an intial
object.  This category is an lccc (as is any linearly ordered set when viewed
as a category).  The full subcategory obtained by removing the initial object
is not reflective: there is no reflection for the initial object.  It is in
the standard sense a complete category.  By every definition I can think of
it is internally complete

In case one is unhappy with this example because the subcategory is only
complete not co-complete, modify the example by adjoining to the ambient
category (and the subcategory) a new formal initial ofject.  The previous
initial object still lacks a reflection.
                                                    Peter Freyd

Subject:     Bulgarian visas
Date: 17-DEC-1990 21:17:52.52
From: "Fred E.J. Linton" <FLINTON@Wesleyan.bitnet>

Got back from two weeks in Warsaw a week ago.

There I learned (from the Bulgarian consulate in Warsaw) that
Bulgaria no longer requires visas of US citizens.

This information (if true -- I have not yet checked it out locally)
may be of interest to others contemplating attending the March EECS '91
outside Sofia.
                                    -- Fred

Fred E.J. Linton  Wesleyan U. Math. Dept.  649 Sci. Tower  Middletown, CT 06457
E-mail:  <FLINTON@eagle.Wesleyan.EDU>  or  <fejlinton@{att|mci}mail.com>
Tel.:         + 1 203 776 2210 (home)  or  + 1 203 347 9411 x2249 (work)

Subject:     CATEGORY THEORY 1991:  SECOND ANNOUNCEMENT
Date:        Sun, 23 Dec 90 12:30:17 EST
From:        Tom Fox <MT16@MUSICA.MCGILL.CA>

                  CATEGORY THEORY 1991:  SECOND ANNOUNCEMENT

                                  June 23-30, 1991

                           McGill University, Montreal, Canada



INVITED SPEAKERS  The following invitees have agreed to speak:
S. Abramsky, A. Carboni, J. Isbell, J. Jardine,F. Lamarche, G. Meloni,
E. Moggi, J. Pelletier, A. Pitts, R. Street, V. Trnkova, R. Wood .

ABSTRACTS  If you wish to give a talk, you must submit an abstract
no later than March 15, l99l.  Abstracts may be sent by mail, email,
or fax to the address given below.  The scientific committee will
announce a list of speakers by May 1.

ACCOMMODATIONS  Private dorm rooms are available at a cost of $32
Canadian per night for professors and $100 a week for students.
Family members are welcome.  Hotel rooms are also available at
$85-$120 per night for a single or double room.  Please make your
reservation with us no later than May 1, indicating the type of
accommodation required and approximate dates of arrival and departure.
We will need a deposit for one night's accommodation.

REGISTRATION FEE  The conference fee will be $150 Canadian ($50 for
students).  After May 1, there will be an additional late
registration fee of $25.

PAYMENT  Payment may be made by check, money order, or bank draft
in Canadian or American dollars (at current exchange rates) to
"Category Theory 1991".  Please mail your registration fee and
deposit for accommodations to us at the address given below.

INFORMATION  If you need further information, please contact us
at the address given below.



CATEGORY THEORY 1991                            Email:  mt16@musica.mcgill.ca
Math Dept, McGill University                    Fax:    (1-514) 398-3899
805 Sherbrooke St W                             Tel:    (1-514) 398-3806
Montreal, Quebec
CANADA  H3A 2K6

Subject:     Re: full internally complete sub-lccc-s
Date: Sun, 23 Dec 90 11:58:06 +0100
From: Thomas Streicher <streiche@unipas.fmi.uni-passau.de>

Reply to Peter Freyd's answer to my question about full internally complete sub-
lccc-s :

the example you have given is a perfectly good answer to the question for the
nonfibred or noninternal case.
What you have actually done is to give a lccc together with a full subcategory
which is not reflective but small complete when looked at it externally from
the point of view of the category of sets.
Actually Peter Johnstone has constructed a similar example, namely  On + On*
where  On  is the linear order of all ordinals and  On*  is the opposite categor
The nonreflective full subcategory which is small complete is of course  On*.
Your example is nearly the same but even a little bit more economical by choos-
ing the one element category instead of  On.

Now why am I not quite satisfied. You have given a perfectly good answer to my
second (easier!) question, but not to my first and more difficult question.

In your mail you said :

   "By every definition I can think of it is internally complete."

I show a definition of internal completeness w.r.t. which the subcategory you
have shown is not NOT internally complete !

Let  C  be a lccc. Then a full subcategory of C  is given by a class  D  of dis-
play maps, i.e. some class  D  of C-morphisms which is stable under pullbacks
along arbitrary C-morphisms.
That means C gives a full subfibration of the fibration  cod : C^2 -> C .
Now by "internally complete" I mean that the full subfibration as given by D is
complete in the usual sense as defined by J. Benabou.
Expressed in an elementary way that means that the following three conditions
are fulfilled :

(1)  any identity morphism is in D  (internal terminal objects)

(2)  if  f : B -> A , g : C-> A  are arbitrary C-morphisms  and
     p : P -> B , q : P -> C  is the pullback cone for  f  and  g  in  C
     then  if   a : A -|> I  is display map such that  a o f and  a o g  are
     display maps  then  a o f o p (= a o g o q) is a display map, too
     (internal pullbacks)

and finally a condition expressing that the full subfibration has internal
products

(3) if  f : B -> A is an arbitrary  C-morphism  and  a : C -|> B  is a display
    map  'Pi'f(g)  is a display map, too
   (where  'Pi'f  is the right adjoint to  f*, the pullback functor in C) .

Now what I want to have is a lccc C and a class D of display maps such that the
conditions  (1),(2),(3)  are all satisfied  and the cartesian embedding of
the subfibration  cod : D^2 -> C  into  cod : C^2 -> C  has a CARTESIAN left
adjoint.

Now what is the reason that any lccc which is a linear order cannot serve as an
example of the kind I want.
Linear orders with a greatest element although surely lccc-s are highly degener-
ate in the sense that left and right adjoints to pullback functors coincide (!!)
Thus as soon as I have a class of display maps satisfying conditions (1) and (3)
I can prove that any arbitrary morphism is a display map :

let  f : B -> A be an arbitrary morphism,
by (1) the identity morphism  id(B) : B -|> B  is a display map
by (3) we have that  'Pi'f(id(B))  is a display map, too
BUT as 'Pi'f(id(B)) = 'Sigma'f(id(B)) = f o id(B) o f  we know that
f itself is a display map.

So one can see that the constraint of internal completeness is much more stronge
r than the constraint of small completeness.

Perhaps one could formulate the question in terms of 'concrete categories'.

Does it hold that for any full concrete category having small limits which are
inherited from Set that it is already a full reflective subcategory of Set itsel
f ??
If this would hold (and I don't know!) than one could try to show that this
eventual theorem can be internalised in the sense that instead of working with
Set work relative to an arbitrary lccc C a display maps REPRESENT full concrete
fibred categories.

Finally I would say that I am not so sure at all whether such an example can be
found at all.
I would appreciate a proof that is is impossible to find such an example even
more.
Some indication is given by the following fact. In Set the only full reflective
subcategories closed under binary products, exponentiation and equlaisers are
isomorphic to { {}, {{}} } . Be careful with "closed under exponentiation I mean
that if A is in the subcategory and X is arbitrary then  X => A  is in the sub-
category !
Ok, in the category of 'w'-sets this is not quite true because of the full sub-
category of per-s. There is even an internally complete full subcategory of 'w'-
Set which is not small but nevertheless reflective. It is obtained by taking the
FREYD COVER of the 'w'-Set model. There propositions are sums of families of set
s indexed over pers. This can be easily seen to be large, but nevertheless refle
ctive.

Perhaps one can show the following weak version of what holds in Set.

Any full internally complete subcategory of an lccc in the fibrational sense is
already reflective.

In Set it is not only reflective but highly trivial, namely a (pre-)order.

Proving this would be a considerable strengthening of FAFT in a special case !!


                                                               Thomas Streicher

Subject:     Constructivity in Computer Science Conference
Date:         Fri, 21 Dec 90 16:32:46 CST
From:         Paul Myers <PMYERS@TRINITY>



Call for Papers ...

Constructivity in Computer Science

Trinity University
San Antonio, Texas
June 18 - 22, 1991

Sponsored by  The University of Chicago and Trinity University

The emergence of computer science as a discipline has naturally led to
a renewal of interest in constructivity, which has become common in
the literature of theoretical computer science, programming language
semantics, database, logic programming, etc.  Constructive notions
form a foundational framework for the field of computer science.
Indeed, constructivity shows up often in the various theoretical (and
applied!) computer science conferences; hence the pertinent results
and ideas have been scattered throughout the literature.  So the time
seems overdue to acknowledge the importance of constructivity to computer
science with a conference linking the two by name (that name derived
from Heyting's first 1957 conference, "Constructivity in Mathematics").

The primary goal of the conference is to provide a forum for the
presentation of contemporary research linking constructivity with
computer science and to establish networks of like-minded researchers
in computer science, logic, and mathematics.  As meetings devoted to
constructivity are infrequent (roughly once a decade), instances of
breadth will be welcome at the conference also.  Robert Constable
(Cornell University) and Michael O'Donnell (University of Chicago)
have agreed to contribute to these endeavors.

Since constructivity is seen by many to be foundational for the field,
it seems important to introduce it explicitly into the computer science
curriculum.  To this end the conference will also include a small "track"
to address integration of the concepts of constructivity into the computer
science curriculum.  Newcomb Greenleaf (Columbia University) has agreed
to contribute in this regard.

Authors should submit 3 copies of an extended abstract by
January 31, 1991 to:

Research:
Michael J. O'Donnell  Department of Computer Science
The University of Chicago
Chicago, Illinois   60637
(312) 702-6011
odonnell@tartarus.UChicago.edu

Curriculum:
J. Paul Myers, Jr.
Department of Computer Science
Trinity University
San Antonio, Texas  78212
(512) 736-7398
BITNET: pmyers@trinity

Submissions should be limited to 10 typed, double-spaced pages. They
should begin with a brief statement of the significance of the submission,
understandable to non-specialists.  Acceptance decisions will be
communicated by April 30, 1991; the final copy will be due at the
conference.  We expect to publish the Proceedings as a volume of
Springer-Verlag's Lecture Notes in Computer Science.

For general information about the conference, please contact Professor
Myers, above.

-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
J. Paul Myers, Jr.                        Department of Computer Science
Trinity University                                     715 Stadium Drive
San Antonio, Texas 78212                                  (512) 736-7398
-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

Subject:     weak intensional identity types
Date: Sat, 29 Dec 90 16:10:38 +0100
From: Thomas Streicher <streiche@unipas.fmi.uni-passau.de>

When considering the "perversities" of Martin-Loef's intensional identity types
I came across the following problem.
Let C be a contextual category (in the sense of Cartmell, see e.g. his paper in
APAL) with perhaps some additional structure such as sums or products of familie
s of types (see e.g. Chapter III of his Cartmell's Thesis or my Thesis for a mor
e recent reference) then we say that C has weak intensional identity types iff w
e have the following structure :

for any object  I  of  C  different from the canonical termina object of level 0
there is a choice of an object Id(I) |> p(I)*I  and a morphism  r(I) : I -> Id(I
)  such that

(1)    p(Id(I)) o r(I) = delta(I) : I -> p(I)*I

       where  p(p(I)*I) o delta(I) = id(I)
       and    q(p(I),I) o delta(I) = id(I), i.e.  delta(I) is the
                                                  fibrewise diagonal

and

(2)    for any object  A |> p(I)*I  and morphism  f : I -> A
                                            with  p(A) o f = delta(I)

       there is a choice  J(f) : Id(I) -> A  of a morphism such that

       J(f) o r(I) = f      and      p(A) o J(f) = p(Id(I))

and

(3)    the Beck condition is satisfied for these data, i.e.

       for any morphism  g : K -> J  where  I |> J  we have

               g*Id(I) = Id(g*I)

               g*r(I) =  r(g*I)

               g*J(f) = J(g*f)  for any morphism  f : delta(I) -> p(A)  .


Notice that the weakness arises from the restriction that  A |> p(I)*I  instead
of  A |> Id(I), i.e. the family for which one considers J-elimination does not
depend on a proof object of type  Id(I).
This definition of weak intensional identity types is nearly literally the
 sameas the one
given by Lawvere in his famous paper from 1970

Equality and Comprehension as Adjoint Functors.

The only difference is that we are working in a framework somewhat more special
than hyperdoctrines and that we do not require uniqueness of elemination.

My PROBLEM now is that up to now I have been unable to find a contextual catego-
ry with, say products of families of types, where one can NOT define weak inten-
sional identity types.
I have found a model where one has weak intensional identity types, but not stro
ng ones. Simply take as types the set of all closed lambda terms modulo beta-
conversion and and the empty set.

But to get rid even of weak intensional identity types seems to be much harder
for the following reasons.

As soon has one can embed a contextual category of the kind considered above in-
to a model of the calculus of constructions where the old types are exactly the
propositions now, then one can define weak intensional identity types by Leibniz
equality !
If one considers models where no real type dependency occurs then one can intro-
duce even strong intensional identity types by putting  Id(A,t,s) = N1, the type
containing exactly one element.Especially, that means that if one considers int-
ensional identity types then there no real need for type dependency arises !! We
are back at old-fashioned Kleene realisability.

Now what could be a way out of this dilemma. There are 2 possibilities (at least
I guess) :

(1)  find a collection TYPE of pers on the natural numbers or some other partial
     combinatory algebra such that the product of a family of pers in TYPE  inde
     xed over some per in TYPE is guaranteed to be in TYPE again

     BUT that's not so easy as

     -  TYPE  must  not  be reflective          and
     -  the collection of pers having only finitely many equivalence classes

        does not do the job of providing a counterexample as well

(2)  the other possibility is to consider the model where types are arbitrary
     cpo-s, i.e. posets where any directed subset has a supremum, without any
     requirements as being finitely based or so

     and families of types are continuous fibrations.

     This model surey gives rise to a contextual category with products of
     families of types.
     But up to now I have'nt been able to see that one cannot find weak intensio
     al identity types within that model.

     It si not so easy as if one restricts oneself to Scott domains then one has
     even strong intensional identity types (see a paper in APAL by Palmgren &
     Stoltenberg-Hansen following a suggestion of Martin-Loef himself).
     The trick is to define for a Scott domain  D  and objects  d1, d2  in  D
     the domain  Id(D,d1,d2)  as the collection of all objects d approximating
     BOTH  d1  and  d2.
     Of course, this trick can be made whenever the cpo has suprema of bounded
     subsets !
     But what happens in the case that there are several different best approxi-
     mating elements to a given couple of elements ???

Even if the concept of intensional identity types seems to be a little bit stran
ge from the point of view of "non-split" category theory, I think it makes per-
fectly good sense from the point of view of "split category theory", namely con-
textual categories.
Therefore I'd more than appreciate any hints on this problem.
For those which are more interested in the topic I have some notes on identity
types in ITT. Unfortunately they are not typed in a way that I can easily put
them on e-mail, but I could easily distribute them by ordinary mail or fax.

                                                             Thomas Streicher
