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" 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: or 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 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 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 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 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