December 1990 - Categories - categories.org.au

Bulgarian visas
by Fred E.J. Linton 11 Jan '91

11 Jan '91

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(a)eagle.Wesleyan.EDU> or <fejlinton(a){att|mci}mail.com> Tel.: + 1 203 776 2210 (home) or + 1 203 347 9411 x2249 (work)

1 1

weak intensional identity types
by Thomas Streicher 30 Dec '90

30 Dec '90

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

1 0

CATEGORY THEORY 1991: SECOND ANNOUNCEMENT
by Tom Fox 24 Dec '90

24 Dec '90

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(a)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

1 0

full internally complete sub-lccc-s
by streiche＠unipas.fmi.uni-passau.de 23 Dec '90

23 Dec '90

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

3 2

Constructivity in Computer Science Conference
by Paul Myers 22 Dec '90

22 Dec '90

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(a)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 -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

1 0