April 1999 - Categories - categories.org.au

CTCS '99: Extension of deadline till 7 May 1999.
by Martin Hofmann 24 Apr '99

24 Apr '99

[ apologies from the moderator for the posting delay which makes this almost moot... ] CATEGORY THEORY IN COMPUTER SCIENCE 1999 10-12 September 1999 EDINBURGH, SCOTLAND ********************************************************** **** Submission deadline extended till 7 May 1999 ******** ********************************************************** Dear colleague, Following a number of requests we have decided to postpone the submission deadline for CTCS '99 by two weeks until 7th May 1999. Notification of authors of accepted papers will take place on 18th June 1999. The proceedings will appear at the conference as Electronic Note in Theoretical Computer Science ENTCS (http://www.elsevier.com/locate/entcs) ENTCS have encouraged us to guest-edit a special issue of Theoretical Computer Science (TCS) consisting of journal versions of selected papers after the conference. The full call for papers can be found under http://www.dcs.ed.ac.uk/home/ctcs99 Martin Hofmann Laboratory for Foundations of Computer Science JCM, Rm 1606 The King's Buildings Mayfield Rd Edinburgh EH9 3JZ UK Phone: +44 131 650 5187 Fax: +44 131 667 7209 E-mail: mxh(a)dcs.ed.ac.uk WWW: www.dcs.ed.ac.uk/home/mxh

1 0

Research Positions
by Matthew Hennessy 23 Apr '99

23 Apr '99

____________________________________________________ My apologies if you receive this more than once! ____________________________________________________ UNIVERSITY OF SUSSEX RESEARCH FELLOWS IN THE FOUNDATIONS OF COMPUTING Two Research Fellows are required for a 2-year project entitled ``The Semantic Foundations of Mobile Computation'', under the direction of Prof. M. Hennessy and funded by the EPSRC. The project objectives include - the development of abstract foundational calculi for mobile systems in which the concepts of location, mobility, failure and security play an central role - the elaboration of behavioural equivalences for these calculi, and their associated algebraic theories - the construction of proof systems and methodologies for establishing properties of mobile systems. The project will start on 1/10/99 and salary will be related to the academic 1A scale. A Ph.D. in Computer Science or Mathematics or equivalent experience is required. In addition to normal research duties the successful candidate will be expected to provide some assistance to undergraduate teaching. To apply please submit applications to Matthew Hennessy School of COGS University of Sussex Falmer Brighton BN1 9QH UK Tel: +44 01273 678101 email: matthewh(a)cogs.sussex.ac.uk from whom more details of the project and the conditions of service are available. Applications should include - a detailed curriculum vitae, - names of three referees with their email addresses, - a statement outlining the candidates proposed contribution to the goals of the project, - copies (or URL references) of any relevant publications.

1 0

Workshop: "OPERADS AND APPLICATIONS",
by I. Moerdijk 21 Apr '99

21 Apr '99

ANNOUNCEMENT: On June 10-12 (Thurday-Saturday), 1999, an informal workshop will take place at University of Utrecht, The Netherlands, under the title "OPERADS AND APPLICATIONS", organized by F. Clauwens (Nijmegen), E. Looijenga and I. Moerdijk (Utrecht). Invited lectures will be given by: A. Joyal M. Kapranov I. Kriz J.-L.Loday M. Markl J. Morava T.Pirashvili S. Shnider J. Stasheff A.Voronov Further information is available via the home page of our institute (http//www.math.uu.nl/operads/). There is no registration fee. Unfortunately, we will not be able to provide funding for participants other than the speakers listed above. If you wish to attend, please register with Corrie van Os (os(a)math.uu.nl) If you do so before April 26, she will be able to book a hotel room for you. Ieke Moerdijk.

1 0

WAIT99 - Call for Papers
by Gabriel Baum 19 Apr '99

19 Apr '99

Please find below the WAIT'99 Call for Papers. We apologize if you receive this message more than once. Call for Papers 28 JAIIO - WAIT'99 Argentinian Workshop on Theoretical Computer Science Buenos Aires - Argentina September 6-7, 1999 ---------------------------------------------------------------------------- --------- The 3rd Argentinian Workshop on Theoretical Computer Science (WAIT'99) will be part on the 28th Argentinean Conference on Informatics and Operations Research (28 JAIIO), to be held in Buenos Aires from September 6th to September 10th, 1999. The goal of the workshop is bringing together researchers from academy (from Argentinean and other universities) and industry professionals in order to discuss theoretical, empirical and experimental results on the field of theoretical computer science. This workshop will consist of invited talks and technical presentations. Contributions are expected in all the areas of theoretical computer science, including the following: * Logical and algebraic foundations for computer science (logics for computer science, category theory, relation algebras, type theory, etc.), * Formal program construction (formal specification of sequential and concurrent programs; analysis, verification and transformation of programs, etc.), * Algorithms and data structures (sequential, parallel, distributed, on-line, probabilistic, etc.), * Computational complexity, * Automata theory, * Graph theory, * Symbolic and algebraic computation. The expected contributions will describe original results as well as undergoing research and development projects on theoretical computer science coming from academy and industry. Papers will be refereed by the International Program Committee, based on the following: * Papers reporting research / experimental results: these papers must present previously unpublished results and will be judged based on their originality, significance, relevance and clarity of presentation. Authors must submit an extended abstract of up to 4 pages containing enough information to allow the referees to determine the merits of their work. It is also allowed to submit the full paper of up to 12 pages including figures and references. * Research projects: aiming to fostering the cooperation among national and foreign researchers, short papers describing ongoing research will be considered. Papers in this category may report already published results. In that case, the authors must include the corresponding references. * Industrial / Commercial applications: also relevant are papers describing applications of theoretical results to real-life situations. Short papers describing results that are both of significance for industry and that make novel or defying applications of theoretical results are sought. INVITED SPEAKERS Thomas S. E. Maibaum (Imperial College, London, UK) Bernhard Moeller (Universitaet Augsburg, Germany) INSTRUCTIONS FOR AUTHORS: In order to facilitate the widest dissemination of the papers, authors are recommended the use of the English language. Nevertheless, papers in Spanish or Portuguese are also welcome. The deadline for submission of papers is May 3rd, 1999. Papers must be submitted electronically in PostScript format (ghostview-readable) to the e-mail address: wait99(a)sol.info.unlp.edu.ar Authors must send in a separate message in ASCII format the following: title of the paper, name and affiliation of all the authors, their e-mail addresses, phone and FAX numbers, an abstract of their contribution of at most ten lines, a list of keywords that best describe the paper, and also the category within which the paper is to be evaluated. Alternative ways for paper submission are possible and must be discussed with the workshop co-chairs. The format for camera-ready papers will be announced with the letter of acceptance. IMPORTANT DATES: Deadline for reception of papers....................May 3rd, 1999 Notification of acceptance..........................June 15th, 1999 Deadline for reception of camera-ready versions.....July 16th, 1999 WORKSHOP CO-CHAIRS: Prof. Gabriel Baum LIFIA Dto. de Informatica Universidad Nacional de La Plata Calle 50 y 115 1er piso. (1900) La Plata - Argentina Tel/Fax : +54-21-22-8252 e-mail: gbaum(a)sol.info.unlp.edu.ar Prof. Marcelo Frias Dpto. De Computacion -FCEyN- Universidad de Buenos Aires Pabellon I - Ciudad Universitaria 1428- Buenos Aires - ARGENTINA Tel/Fax : +54-1-783-0729 e-mail: mfrias(a)sol.info.unlp.edu.ar PROGRAM COMMITTEE: Gabriel Baum (Universidad Nacional de La Plata, Argentina) Javier Blanco (Universidad Nacional de Cordoba, Argentina) Luis FariÃ±as del Cerro (Universite Paul Sabatier, France) Esteban Feuerstein (Universidad Nacional de Buenos Aires and Universidad Nacional de General Sarmiento, Argentina) Marcelo Frias (Universidad Nacional de Buenos Aires, Argentina) Armando Haeberer (Pontificia Universidade Catolica de Rio de Janeiro, Brazil) Edward Hermann Haeusler (Pontificia Universidade Catolica de Rio de Janeiro, Brazil) Joos Heintz (Universidad Nacional de Buenos Aires, Argentina) Roger Maddux (Iowa State University, USA) Tom Maibaum (Imperial College, UK) Bernhard Moeller (Universitaet Augsburg, Germany) Gonzalo Navarro (Universidad de Chile, Chile) Alfredo Olivero (Universidad Nacional de Buenos Aires and Universidad Nacional de General Sarmiento, Argentina) Ruy de Queiroz (Universidade Federal de Pernambuco, Brazil) Alvaro Tasistro (Universidad de la Republica, Uruguay) Sergio Yovine (CNRS-VERIMAG, France) For more information send e-mail to: jaiio(a)sadio.edu.ar, write to: SADIO / WAIT'99 Uruguay 252 2D 1015 - Buenos Aires ARGENTINA TEL: +54-1-3715755/4763950 FAX: +54-1-3723950 or see http://www.uba.ar/wwws/sadio ___________________________________________ Gabriel Baum LIFIA Facultad de Ciencias Exactas Universidad Nacional de La Plata Calle 50 y 115 - 1er piso (1900) La Plata e-mail: gbaum(a)sol.info.unlp.edu.ar Tel/Fax: +54 21 228252 ___________________________________________

1 1

small universes
by cxm7＠po.cwru.edu 13 Apr '99

13 Apr '99

Has anyone considered this idea for smaller Universes? Maybe it is well known but I had not seen it. We can drop the "replacement" condition on a Grothendieck universe U: for every x in U and every onto function h:x-->y with y a subset of U, y is also a member of U. It is enough if a universe naturally models Zermelo set theory. (Or even a bit less, as in the elementary theory of the cagtegory of sets.) So we could define a "universe" to be any set of the form V(i) for i a limit ordinal (greater than omega). Here V(i) is the set of all sets with rank less than i. Then the claim "each set is member of some universe" is simply a theorem of ZF. This is a great deal weaker than Grothendieck's axiom as stated in SGA. Grothendieck's is equivalent to extending ZF by a proper class of inaccessible cardinals. Each of these "universes" models Zermelo set theory (i.e. ZF without the replacement axiom but with separation) and a bit more. Insofar as general category theory is provable in Zermelo set theory, it applies to the U-small categories for each universe U in this sense. I believe all the apparatus of Grothendieck's TOHOKU paper, and the topos theory and cohomology of the SGAs, is provable in Zermelo set theory with axiom of choice. So this definition of universes formalizes current cohomological number theory just as Grothendieck suggested, within the axioms ZFC. The only thing I want to check (as soon as I get to my office) is Grothendieck's proof that every AB5 category has enough injectives--it is an induction with a proper class of steps but you prove it is fixed after some set of steps. Possibly you need the axiom of replacement to show it is indeed a set of steps. I cannot think of any other result in this part of category theory that could require replacement. So, is this all old news? Or does anyone see a problem here that I am missing?

2 1

AMS Buffalo April 24/25, 1999
by F W Lawvere 12 Apr '99

12 Apr '99

LAST ANNOUNCEMENT SMOOTH CATEGORIES IN GEOMETRY AND MECHANICS Special session of AMS Meeting No. 943 in Buffalo, N.Y. Diefendorf Hall, SUNY, Main Street Campus April 24/25, 1999 note: changes in Sunday schedule SCHEDULE: Saturday, April 24, 1999 9:00 - 9:20 James FARAN: A Synthetic Approach to Characteristic Cohomology (Abstract # 943-18-72) 9:30 - 9:50 Hirokazu NISHIMURA: Infinitesimal Calculus of Variations (Abstract # 943-18-71) 10:00 - 10:20 Jonathon FUNK: Lebesgue Toposes (Abstract # 943-18-65) 10:30 - 10:50 George JANELIDZE: (joint work with Walter Tholen) Strongly Separable Morphisms (Abstract # 943-18-73) *** 2:30 - 2:50 Gonzalo REYES: (joint work with Anders Kock) Atoms and Categories of Differential Equations in SDG (Abstract # 943-18-109) 3:00 - 3:20 Felipe GAGO: Transversal Stability for Infinitesimally Represented Germs (Abstract # 943-18-66) 3:30 - 3:50 Anders KOCK: Infinitesimal Geometric Aspects of Riemannian Metrics (Abstract # 943-18-68) *** 4:30 - 4:50 Rene LAVENDHOMME: Infinitesimal Deformations in SDG (Abstract # 943-18-70) 5:00 - 5:20 Marta BUNGE: Single Universe for Intensive and Extensive Quantities in a Topos (Abstract # 943-18-76) Sunday, April 25, 1999 9:00 - 9:20 Peter FREYD: Arithmetic Categories (Abstract # 943-18-69) 9:30 - 9:50 Craig SNYDAL: Vertex Algebras, an Example of a Relaxed Multilinear Category (Abstract # 943-18-67) 10:00 - 10:20 Walter NOLL: Conceptual Mathematics, Categories, Functors, and Tensors (Abstract # 943-18-176) 10:30 - 10:50 Bill LAWVERE Smoothness of Cubical Splines (Abstract # 943-18-145) ***** 2:30 - 4:00 Round Table Discussion on the Theme of the Special Session ARRIVAL DATE: Friday, April 23, 1999 BUFFET DINNER: Saturday, April 24, 6:30 p.m. - 11 p.m. at the Center for Tomorrow on UBs North Campus. Cost $ 10.--; cash bar. Transportation available from Diefendorf Hall. LUNCHES: available for both days at Diefendorf Hall. ACCOMODATIONS: For the participants of the meeting the downtown HYATT REGENCY BUFFALO has special rates. For more information about hotels, etc. see Http://www.acsu.buffalo.edu/~jjfaran/AMS_MEETING_home.html A block of rooms under the name AMS SMOOTH CATEGORIES has been reserved at the UNIVERSITY MANOR, 3612 Main Street, (intersection Main/Bailey, at walking distance from Main Street Campus). Prices are: Queen US$ 50.--/ King or 2 beds US$ 54.--, minus 10% for participants, plus 13% tax. Tel. (716) 837-3344; Fax (716 )834-6246. REGISTRATION: Room 114, Diefendorf Hall, Saturday starting at 7:30 am. Fees are $ 30.--/AMS or CMS members, $ 45.-- /nonmembers, $ 10.-- emeritus members, students, unemployed mathematicians, (payable on-site only) ******************************************************************************* F. William Lawvere Mathematics Dept. SUNY wlawvere(a)acsu.buffalo.edu 106 Diefendorf Hall 716-829-2144 ext. 117 Buffalo, N.Y. 14214, USA *******************************************************************************

1 0

email
by Michael Barr 09 Apr '99

09 Apr '99

I have a new email address, as above. This new address will be given ONLY to genuine correspondents. Although the addresses at math and triples will remain valid, I will eventually route all mail that does not go to the barrs address to my spam file to be looked at once or twice a week and all spam deleted. This is because I have begun to receive a half dozen spams a day. ------------------------------------------------------------------- History shows that the human mind, fed by constant accessions of knowledge, periodically grows too large for its theoretical coverings, and bursts them asunder to appear in new habiliments, as the feeding and growing grub, at intervals, casts its too narrow skin and assumes another... Truly the imago state of Man seems to be terribly distant, but every moult is a step gained. - Charles Darwin, from "The Origin of Species"

1 0

Re: incompleteness of ZF
by Thomas Streicher 08 Apr '99

08 Apr '99

Dear Paul, a short reply to your mail about inconsistency of replacement. As Paul has already remarked in his mail the type-theoretic counterpart of replacement is that of universe `a la Martin-Loef. As in case of replacement the use of universes is that they allow for construction of families of types (as e.g. needed for inverse limit constructions in Domain Theory which cannot be performed in pure topos logic precisely for this reason). But as already observed in a survey article by Thierry Coquand (ftp://ftp.cs.chalmers.se/users/cs/coquand/meta.ps.Z) and, surely, known to Martin-Loef himself it holds that in type theory with n+1 universes one may prove the consistency of type theory with n universes simply by constructing a model using the n+1st universe. But, of course, this extra universe is needed for the consistency proof. Accordingly, one cannot prove the consistency of type theory with $\omega$ universes without postulating an $\omega$th universe. Quite the same phenomenon is going on in set theory as already pointed out by some previous replies. However, in set theory due to the presence of ``impredicative'' axioms the proof theoretic strength is incredibly stronger than set of Martin-Laoef type theory with $\omega4 universes. Best, Thomas

5 4

Position at Ottawa U.
by Phil Scott 06 Apr '99

06 Apr '99

The Department of Mathematics and Statistics of the University of Ottawa is expecting one, if not several, temporary positions for the upcoming year. The most significant is the Canadian Mathematical Society Fellowship. This is a 3 year position (1 + renewable for 2 years), at the level of Assistant Professor, with a reduced teaching load of 1 course per semester available July 1. This position recently became available when the current holder moved elsewhere. There may also be one or more temporary positions pending budgetary approval. We are hopeful to attract candidates interested in one or more of the following fields: 1. Categorical and Linear Logic 2. Theoretical Computer Science 3. Tensored Categories We are also members of the Category Theory Centre in Montreal (Team members and colleagues include: M. Barr, M. Bunge, T. Fox, J. Lambek, M. Makkai, P. Panangaden, G. Reyes, R. Seely). The category team has weekly seminars (Ottawa is 2 hours from Montreal). We shall also be having frequent seminars of our team here at U. Ottawa. If you are interested, please contact one of us by email right away: Prof. R. Blute Prof. P. Scott rblute(a)mathstat.uottawa.ca phil(a)mathstat.uottawa.ca Thanks. We hope to hear from you soon. Rick Blute and Phil Scott

1 0

Is Zermelo-Fraenkel set theory inconsistent?
by Paul Taylor 02 Apr '99

02 Apr '99

IS ZERMELO-FRAENKEL SET THEORY INCONSISTENT? At the end of this message is a sketch of an argument that leads to the conclusion that Zermelo-Fraenkel set theory is inconsistent. The impact on mathematics is not as devastating as the incautious observer might suppose. Recall that ZERMELO set theory (1908), which is essentially equivalent to the categorists' notion of ELEMENTARY TOPOS with natural numbers and the axiom of choice, is adequate for most of the purposes of mathematics, though not, as I shall try to explain, logic (and theoretical computer science). ZERMELO-FRAENKEL set theory is the extension of this system by the axiom-scheme of REPLACEMENT, which was first formulated by Adolf (later Abraham) Fraenkel, Nels Lennes and Thoralf Skolem in 1922, although Dimitry Mirimanoff already had something of the idea in 1917. Notice that this is some two decades after the appearance of the famous "antinomies" of set theory, so presumably the set theorists' guard had dropped by that time, and they had begun again to assert megalomaniac axioms. On the other hand, it is a decade before the second generation of paradoxical results, Godel's incompleteness theorem and Turing's unsolvability of the Halting Problem. Whenever I see set theory books in a library or bookshop, I turn to the index to find out what they have to say about Replacement. Usually there is some trivial result, such as the existence of what categorists call image factorisation, that could have been proved from Zermelo's axioms with a little more facility in set-theoretic constructions. The basic use of Replacement, that you will find in the better set theory books, is the recursive construction of sets (in substance -- types or objects to type-theorists and categorists -- rather than their names). For example, Mostowski's theorem states that every well founded extensional binary relation < is isomorphic to the membership relation for a unique transitive set. This is found, recursively, by means of the formula f(x) = { f(y) | y < x }, which also provides the extensional reflection (quotient) of any well founded relation. In fact the latter result (where the quotient relation is merely another relation, rather than a membership relation) can be proved using the topos or Zermelo axioms alone, and not Replacement [1], although there are categorical generalisations of this that certainly do need Replacement. Richard Montague [2] proved a result that should have been taken as a warning of the perilous nature of Replacement, though I suspect that Montague's personal eccentricities may have been the reason why he was ignored. ZF can prove the consistency, not only of Zermelo set theory (Z) itself, but also of Z extended by any single theorem of ZF. Adrian Mathias has claimed [3] that Bourbaki was "ignorant" of Replacement, ie that it did not occur in "Theorie des Ensembles" [4]. Although Bourbaki is hardly very clear on this matter, it does include a version of Replacement in its axioms, indeed one that is in widespread use in category theory and other parts of mathematics, namely that one can form the UNION of any SET-INDEXED FAMILY of SETS. One application of N-indexed unions in theoretical computer science is Scott's "D-infinity" construction of models of the untyped lambda calculus. Starting from any domain D0=D, one may form its function-space D1=(D0->D0), and similarly D2=(D1->D1), etc., linking these together with embedding- projection pairs. If D was one of the examples of L-domains, having a pair of elements with infinitely many minimal upper bounds, then one can show (classically) that D-infinity has the cardinality of a model of Zermelo set theory, so need not exist within such a model unless it also satisfies Replacement. These two ways of seeing Replacement have a common theme: we use N-indexed or transfinite unions to unfold a free(ish) model of one logic within a model of another. Having seen this in the context of a messy domain-theoretic construction, we may think in a more disciplined way about free models of the lambda calculus, the topos axioms, etc. In fact, there is no difficulty in constructing these models, as they are merely TERM ALGEBRAS. The problem lies in proving that the term algebra has the universal (initiality) property that qualifies it as "free": Let S be the universe (the category of ZF-sets, for example) and F the term algebra (internal to S) for the logic L. Suppose that S itself is a model of L. Then there is a unique interpretation functor []:F->S that takes each syntactic operation of F (eg prod(a,b)) to the semantics ([a] x [b]) in S. It is merely unique up to unique isomorphism if the L-structure in S is defined by universal properties rather than being chosen. This initiality property may also be expressed type-theoretically. Per Martin-Lof [5] introduced objects with such a property, called UNIVERSES, observing the analogy with Replacement. This point of view stresses that the above property is a RECURSION SCHEME. Let me explain how I came to realise that the existence of []:F->S depends, in general, on Replacement. There is an amazingly simple but incredibly powerful argument, due to Peter Freyd and known variously as (Artin-Wraith) glu(e)ing, sconing, the Freyd cover, logical relations and other names. It is based on some very elementary categorical investigations of a certain comma category involving F and S. This argument has been developed rather a long way (the most recent paper that I know of is [6]), and we are pretty close to having a purely categorical proof of the strong normalisation theorem for lambda calculi that, unlike the syntactic proofs, is completely generic with regard to the calculus in question. Freyd originally showed that the terminal object (1) of the free topos (F) is projective, and more generally the "global sections functor" F(1,-) : F -> S preserves colimits. In particular, it preserves the initial object (0), which is categorical jargon for saying that S proves the consistency of F, because the S-set of F-morphisms 1->0 is the initial (empty) S-set. I found this suspicious, because the punch-line of Andre Joyal's 1973 (but as yet unpublished and unavailable) categorical proof of Godel's incompleteness theorem is that such a functor F(1,-) : F -> S does *not* preserve the initial object. The more careful amongst categorists ought also to be suspicious when I speak of "a functor F(1,-) or [] : F -> S" where F is an INTERNAL category in S. The meaning that we must give to this phrase is that it is "syntactic sugar" for a certain FIBRATION p: V -> F, where V is also an internal category and p and internal functor in S. This brings us back to the relationship between Replacement as a recursive construction of objects and Replacement as infinitary colimits: "p: V -> F" is the colimit (in a 2-category whose objects are fibrations) of a recursively defined diagram vaguely similar to that which gives Scott's D-infinity. I have come to the conclusion that attempts to define "colimits" such as this are inherently circular: what, after all, does it mean to have a "cocone" to test such an alleged colimit? My categorical formulation of Replacement speaks about fibrations and smaller colimits defined internally in the style of Benabou. This is to be found in the final section (9.5) of my book [7], Section 7.7 of which also gives an account of Freyd's gluing construction. This book is officially due to be published in mid-May, but it is already in stock (and I have my own copy in front of me), and is available direct from the publishers at 50 pounds (inclusive of overland postage and packing). Please contact Richard Knott, email: rknott(a)cup.cam.ac.uk fax: +44 1223 315 052 tel: +44 1223 325 916 (but other methods are preferable) snail: Cambridge University Press, The Edinburgh Building, Shaftesbury Road, Cambridge, CB2 2RU, UK with your address and credit card number. (2.50 pounds extra for airmail.) Having seen that Replacement provides a UNIFORM way of proving consistency of any fragment of logic, we come at last to the inconsistency argument: Let L(0) be Zermelo set theory (or the axioms for an elementary topos). For each n, let L(n+1) be L(n) plus as much of the axiom-scheme of replacement as is needed to justify the gluing construction that shows that L(n+1) |- ``L(n) is consistent.'' Now let L(infinity) be the union of L(n) over n:N. If L(infinity) |- false then L(n) |- false for some n. But L(infinity) |- ``L(n) is consistent,'' so L(infinity) proves its OWN consistency, contradicting Godel's theorem. However, L(infinity) has a standard non-trivial interpretation in Zermelo--Fraenkel set theory, which is therefore inconsistent. [1] Paul Taylor, Intuitionistic Sets and Ordinals, JSL 61 (1996) 705-44 [2] Richard Montague, Fraenkel's Addition to the Axioms of Zermelo, pp 91--114 of Bar-Hillel, et al., eds., Essays on the Foundations of Mathematics, Magnes Press, Hebrew University, 1966 (distributed by Oxford University Press). [3] Adrian Mathias, The Ignorance of Bourbaki, Mathematical Intelligencer, 14 (1992) 4-13. [4] Nicolas Bourbaki, Elements de Mathematique XXII: Theories des Ensembles, Livre I, Structures, Hermann, 1957 (English translation 1968). [5] Per Martin-Lof, An Intuitionistic Theory of Types: Predicative part, pp 73--118 in Rose and Sheperdson, eds., Logic Colloquium '73, North-Holland, Studies in Logic and the Foundations of Mathematics #80, 1975 [6] Djordje Cubric, Peter Dybjer and Philip Scott, Normalisation and the Yoneda Embedding, MSCS 8 (1998) 153--192. [7] Paul Taylor, Practical Foundations of Mathematics, Cambridge University Press, Cambridge Studies in Advanced Mathematics #59, xii+572pp, 1999. http://www.dcs.qmw.ac.uk/~pt/Practical_Foundations/ Paul Taylor <pt(a)dcs.qmw.ac.uk> 19990401 This message may be copied elsewhere, ON CONDITION that it is quoted in its ENTIRETY.

3 2