From MAILER-DAEMON Sun Mar 30 15:45:59 2003 Date: 30 Mar 2003 15:45:59 -0400 From: Mail System Internal Data Subject: DON'T DELETE THIS MESSAGE -- FOLDER INTERNAL DATA Message-ID: <1049053559@mta.ca> X-IMAP: 1041464799 0000000069 Status: RO This text is part of the internal format of your mail folder, and is not a real message. It is created automatically by the mail system software. If deleted, important folder data will be lost, and it will be re-created with the data reset to initial values. From rrosebru@mta.ca Wed Jan 1 17:26:29 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 01 Jan 2003 17:26:29 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18TqFP-0005QH-00 for categories-list@mta.ca; Wed, 01 Jan 2003 17:17:55 -0400 From: Carl Futia Message-ID: <29.34eb20a6.2b447c13@aol.com> Date: Wed, 1 Jan 2003 12:14:59 EST Subject: categories: Benabou manuscript To: categories@mta.ca Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 1 I have seen several references to an unpublished 1973 manuscript by Jean Benabou on profunctors. I have had no success finding an e-mail address for Prof. Benabou. Does he have one? Peter Johnstone has a very nice synopsis of the subject in his new book in section B 2.7. Francis Borceux has a more elementary treatment of distributors in the first volume of his handbook of categorical algebra. Are there other sources which offer a substantial discussion of profunctors? I would be happy to pay duplication and mailing costs to obtain a copy of the Benabou paper. Thanks for any information you can provide. Carl Futia From rrosebru@mta.ca Thu Jan 2 20:33:29 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 02 Jan 2003 20:33:29 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18UFfK-0005BW-00 for categories-list@mta.ca; Thu, 02 Jan 2003 20:26:22 -0400 Message-ID: <3E13DF3B.59E2@maths.usyd.edu.au> Date: Thu, 02 Jan 2003 17:42:03 +1100 From: Max Kelly Organization: School of Mathematics and Statistics, University of Sydney X-Mailer: Mozilla 3.01Gold (X11; I; OSF1 V5.1 alpha) MIME-Version: 1.0 To: categories@mta.ca Subject: categories: thoughts arising from a letter of Lawvere Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 2 Sorting through old papers after the move to our new house, I came across a communication to Categories by Bill Lawvere, dated 21 Nov 2001, entitled "categories:K-spaces and Hurewich", and concerned with the history of k-spaces and related concepts. I thought the following bit of history worth contributing. Before studying monoidal closed categories in his well-known doctoral thesis, Brian Day wrote a very pleasant Masters thesis on monoidal closed structures on variants of topological spaces. For some reason this never got published - perhaps it was not thought original enough at the time - but it contained the perfect way of introducing k-spaces; and not just hausdorff ones - restricting to those is an error. One starts with the category Top of topological spaces, and the category Comp of compact hausdorff spaces. Based on Comp, one forms Steenrod's category of quasi-spaces: a quasi-space is a set X along with, for each A in Comp, a subset of Set(A,X) whose elements may be called the "allowable" maps - one imposes a few evident axioms on these. The quasi-spaces form a category Qu, whose morphisms from X to Y are those set-maps whose composites with allowables are allowable. This is of course classical; but what Brian had is the following. There is an evident functor f: Top --> Qu; just call A --> X allowable if it is continuous. There is an equally evident functor g: Qu --> Top; call a subset open if its characteristic function into the Sierpinski space 2 lies in Qu. We have the adjunction g --| f. As with any adjunction, we have an equivalence between the full subcategory of Top where the counit is invertible and the full subcategory of Qu where the unit is invertible. The subcategory of Top here, of course reflective in Top, is the category of k-spaces, better called the "compactly-generated" spaces; it is also a coreflective full subcategory of Qu. Others have noticed this since and published it; but certainly subsequent to Brian's 1968 (I think) Master's thesis. Of course one is not obliged to use Comp in defining one's quasi-spaces; write Qu' for the quasi-spaces based instead on Top. Now Top --> Qu' is fully faithful, and reflective: we know the reflexion explicitly. Again Qu' is cartesian-closed, although Top is not. This is how Brian and I proved those results in [On topological quotient maps preserved by pullbacks or products, Proc. Cambridge Phil. Soc.67, 1970, 553 - 558]. We did the pulling back in the cartesian closed Qu', applied the reflexion, and wrote down the condition for preservation. We feared, however, that topologists would be frightened off by these "abstract categorical notions"; so we went through all that we had done, translating it into the usual language of topology, before we submitted it for publication. The readers, with our motives and techniques so concealed, must have thought it black magic. Of course, as Bill Lawvere said, the whole "quasi" business should be done abstractly, and turns out to involve subcategories of presheaf categories, with associated toposes like that of Peter Johnstone. I see that this letter has become very long. I must apologize: but so much of our history is getting lost forever. Max Kelly. From rrosebru@mta.ca Sun Jan 5 17:09:39 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 05 Jan 2003 17:09:39 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18VHvq-0004mJ-00 for categories-list@mta.ca; Sun, 05 Jan 2003 17:03:42 -0400 Date: Sat, 4 Jan 2003 18:34:04 -0500 (EST) From: "NASSLLI'03 Bloomington, Indiana" X-Sender: nasslli@lear.ucs.indiana.edu To: categories@mta.ca Subject: categories: NASSLLI-2003 ANNOUNCEMENT Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 4 Second North American Summer School in Logic, Language and Information NASSLLI-2003 June 17-21, 2003, Bloomington, Indiana http://www.indiana.edu/~nasslli %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% The NASSLLI Steering Committee is pleased to announce the Second North American Summer School in Logic, Language and Information, to be held in Bloomington, Indiana, June 17-21, 2003. The event follows on from the successful first school at Stanford in June, 2002. The school is focussed on the interfaces among linguistics, logic, and computation, broadly conceived, and on related fields. Our sister school, the European Summer School in Logic, Language, and Information, has been highly successful, becoming an important meeting place and forum for discussion for students and researchers interested in the interdisciplinary study of Logic, Language and Information. We hope that the North American schools will follow in this tradition. PROGRAM --------- Marco Aiello, Guram Bezhanishvili, and Darko Sarenac Reasoning about Space (Workshop) Alexandru Baltag Logics for Communication: reasoning about information flow in dialogue games. Roman Bartak Foundations of Constraint Satisfaction Patrick Blackburn and Johan Bos Computational semantics for natural language Gerhard Jaeger and Reinhard Blutner Linguistic and computational issues in Optimality Theory Edward Keenan and Edward Stabler A Mathematical Theory of Grammatical Categories Daniel Leivant Logic of Programs Dov Monderer Games in Informational Form Yiannis Moschovakis Referential intensions: a logical calculus for synonymy John C. Paolillo Statistical models for language: structure and computation Dirk Pattinson An Introduction to the Theory of Coalgebras Ron van der Meyden Algorithmic Verification for Epistemic Logic Courses consist of five sessions of 90 minutes each. NASSLLI courses are aimed at graduate students or advanced undergraduates in computer science, linguistics, logic, philosophy, and related areas. Course abstracts are available from http://www.indiana.edu/~nasslli/program.html In addition, there will be evening lectures and a session of student papers. A Call for Papers for the Student Session will be distributed separately. RELATED EVENTS: NASSLLI'03 will be co-located with TARK'03, the 9th Conference on Theoretical Aspects of Knowledge and Rationality (see http://www.tark.org ). In addition, NASSLLI'03 will be co-located with MoL'03, the 8th Meeting on the Mathematics of Language (see http://grail.let.uu.nl/mol8/ ). Both of these conferences will take place June 20-22, 2003. INFORMATION ON REGISTRATION, ACCOMODATIONS, and SUPPORT should be available from our web site in January, 2003. WEB SITE FOR NASSLLI'03, to be held at Indiana University in June 2003: http://www.indiana.edu/~nasslli/ NASSLLI STEERING COMMITTEE (list in formation) David Beaver Barbara Grosz Phokion Kolaitis Larry Moss Stuart Shieber Moshe Vardi Contact: nasslli@indiana.edu From rrosebru@mta.ca Mon Jan 6 21:10:46 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 06 Jan 2003 21:10:46 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18ViAe-0003iZ-00 for categories-list@mta.ca; Mon, 06 Jan 2003 21:04:44 -0400 Message-Id: <200301061433.h06EXIR00839@mendieta.science.uva.nl> Date: Mon, 6 Jan 2003 15:33:18 +0100 X-Organisation: Faculty of Science, University of Amsterdam, The Netherlands X-URL: http://www.science.uva.nl/ From: info@folli.org To: categories@mta.ca Subject: categories: CfP: ESSLLI'03 Student Session Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 5 !!! Concerns all students in Logic, Linguistics and Computer Science !!! !!! Please circulate and post among students !!! We apologise if you receive this message more than once. ESSLLI-2003 STUDENT SESSION SECOND CALL FOR PAPERS August 18-29 2003, Vienna, Austria Deadline: February 24, 2003 http://www.science.uva.nl/~bcate/esslli03 We are pleased to announce the Student Session of the 15th European Summer School in Logic, Language and Information (ESSLLI-2003), which will be held in Vienna from August 18-29 2003. We invite submission of papers for presentation at the ESSLLI-2003 Student Session and for appearance in the proceedings. PURPOSE: This eighth ESSLLI Student Session will provide, like the previous editions, an opportunity for ESSLLI participants who are students to present their own work in progress and get feedback from senior researchers and fellow-students. The ESSLLI Student Session encourages submissions from students at any level, undergraduates (before completion of the Master Thesis) as well as postgraduates (before completion of the PhD degree). Papers co-authored by non-students will not be accepted. Papers may be accepted for full presentation (30 minutes including 10 minutes of discussion) or for a poster presentation. All the accepted papers will be published in the ESSLLI-2003 Student Session proceedings, which will be made available during the summer school. REQUIREMENTS: The Student Session papers should describe original, unpublished work, completed or in progress that demonstrates insight, creativity, and promise. No previously published papers should be submitted. We welcome submissions with topics within the areas Logic, Language and Computation. FORMAT OF SUBMISSION: Student authors should submit a full paper, written in English, not to exceed 7 pages of length exclusive of references. Note that the length of the final version of the accepted papers will not be allowed to exceed 10 pages. For any submission, a plain ASCII text version of the identification page should be sent separately, using the following format: Title: title of the submission First author: firstname lastname Address: address of the first author ...... Last author: firstname lastname Address: address of the last author Short summary: abstract (5 lines) Subject area (one or two of): Logic | Language | Computation In case the paper is being submitted to another conference or workshop, this must be clearly indicated on the identification page. The paper submission should be in one of the following formats: PostScript, PDF, RTF, or plain text. (In case of acceptance, the final version of the paper will have to be submitted in LaTeX format.) The papers must use single column A4 size pages, 11pt or 12pt fonts, and standard margins, and may not exceed 7 pages of length exclusive of references. Submissions not in accordance with these formatting and length requirements may be subject to rejection without review. The paper and separate identification page must be sent by e-mail to b.ten.cate@hum.uva.nl by FEBRUARY 24th 2003. ESSLLI-2003 INFORMATION: In order to present a paper at ESSLLI-2003 Student Session, at least one student author of each accepted paper has to register as a participant at ESSLLI-2003. The authors of accepted papers will be eligible for reduced registration fees even after the deadline for early registration. For all information concerning ESSLLI-2003, please consult the ESSLLI-2003 web site at www.logic.at/esslli03. IMPORTANT DATES: Deadline for submission of papers : February 24, 2003. Authors notifications : April 22, 2003. Final version due : May 19, 2003. ESSLLI-2003 Student Session : August 18-29, 2003. PROGRAMME COMMITTEE: Laura Alonso Alemany, University of Barcelona Roberto Bonato, University of Verona, University Bordeaux I Balder ten Cate, University of Amsterdam Paul Egre, University Paris I Dan Flickinger, Stanford University Maria Fuentes Forte, University of Girona Gabriel Infante Lopez, University of Amsterdam Jakob Kellner, University of Vienna Favio Miranda-Perea, LMU Muenchen Christian Retore, INRIA, LaBRI Bordeaux Sergio Tessaris, University of Bolzano For more information concerning the ESSLLI-2003 Student Session, please consult the web-site www.science.uva.nl/~bcate/esslli03 . Also, for specific questions do not hesitate to contact me: Balder ten Cate ILLC, University of Amsterdam Nieuwe Doelenstraat 15 1012 CP Amsterdam The Netherlands Phone: +31.20.5254552 Fax: +31.20.5254503 E-mail: b.ten.cate@hum.uva.nl From rrosebru@mta.ca Mon Jan 6 21:10:47 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 06 Jan 2003 21:10:47 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18ViBK-0003kZ-00 for categories-list@mta.ca; Mon, 06 Jan 2003 21:05:26 -0400 From: Uffe Henrik Engberg MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <15897.40262.755809.507259@harald.daimi.au.dk> Date: Mon, 6 Jan 2003 16:14:14 +0100 To: categories@mta.ca Subject: categories: BRICS PhD grants and Marie Curie fellowships X-Mailer: VM 6.90 under Emacs 20.7.1 Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 6 [Please accept our apologies if you receive this more than once] BRICS - Basic Research in Computer Science at the Universities of Aarhus and Aalborg, Denmark This is a call for applications for: PhD admission and PhD grants, and Marie Curie Training Site Fellowships. BRICS, Basic Research in Computer Science, is funded by the Danish National Research Foundation. It comprises an International PhD School with an associated Research Laboratory. BRICS is based on a commitment to develop theoretical computer science, covering core areas such as: - Semantics of Computation, - Logic, - Algorithms and Data Structures, - Complexity Theory, - Data Security and Cryptology, and - Verification, as well as a number of spin-off activities including - Web Technology, - Quantum Informatics, - Bio Informatics, and - Networks and Distributed Real-Time Systems. BRICS has a number of new PhD grants and fellowships available, starting in 2003. Applications can be submitted at any time. However, the application deadline for PhD grants starting August 2003 is February 15, 2003. PhD admission and grants: Any student with at least four years of studies in computer science is eligible to apply for PhD admission and grants. Marie Curie Fellowships: These fellowships are offered within Interactive Computation - Methodology, Security, and Efficiency - and are open to PhD students who are nationals of a member state of the European Community or an associated state, and who wish to spend time (from three months to twelve months) at BRICS, as part of their PhD studies. Further information, including instructions on how to apply, can be found at: http://www.brics.dk/Positions/ For information on BRICS in general, see: http://www.brics.dk/ http://www.cs.auc.dk/research/FS/ You are also welcome to contact one of the BRICS directors: - Mogens Nielsen, Aarhus, mn@brics.dk - Kim G. Larsen, Aalborg, kgl@brics.dk Kindly forward this information to interested students at your university or research institute. Thank you very much. Mogens Nielsen and Kim G. Larsen From rrosebru@mta.ca Wed Jan 8 14:35:03 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 08 Jan 2003 14:35:03 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18WKuH-0000sJ-00 for categories-list@mta.ca; Wed, 08 Jan 2003 14:26:25 -0400 Date: Mon, 6 Jan 2003 18:28:43 -0800 (PST) From: Galchin Vasili Subject: categories: Hereditarily finite sets To: categories@mta.ca Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: RO X-Status: X-Keywords: X-UID: 7 Hello, I would like to know if anybody is doing research on applying category theory to hereditarily-finite sets, e.g. where an object is a hereditarily set with some kind of structure to it and morphism that preserves that structure. Obviously, the subcategory of SET where objects are just hered. finite sets and morphisms are functions between hered. finite sets is not "interesting". Also, the case where an object is a hered. set together with an endomorphism doesn't sound "interesting". I would like URL's of papers if possible. Thank you. Regards, Bill From rrosebru@mta.ca Wed Jan 8 15:29:18 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 08 Jan 2003 15:29:18 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18WLrl-00054m-00 for categories-list@mta.ca; Wed, 08 Jan 2003 15:27:53 -0400 Subject: categories: Category and Scheduling Theory Date: Tue, 7 Jan 2003 15:36:35 +0100 From: "Claus Gwiggner" To: Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: RO X-Status: X-Keywords: X-UID: 8 Hi, is category theory a suited language to express "structure" in scheduling or combinatorial optimisation problems ? Thanks, Claus From rrosebru@mta.ca Wed Jan 8 15:40:45 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 08 Jan 2003 15:40:45 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18WM2s-00067R-00 for categories-list@mta.ca; Wed, 08 Jan 2003 15:39:22 -0400 Date: Tue, 7 Jan 2003 15:08:13 -0500 (EST) From: Phil Scott X-Sender: phil@dinats To: categories@mta.ca Subject: categories: Field's Institute Summer School in Logic & Theoretical CS Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 9 Dear Colleagues: June will be theoretical computer science month at U. Ottawa! The Field's Institute will sponsor a summer school in Logic and Foundations of Computation at the University of Ottawa this summer, June 2-20, 2003. This program will be hosted by the logic group in the Department of Mathematics and Statistics at the University of Ottawa (consisting of Philip Scott, Richard Blute, and Peter Selinger). The program will consist of 2 weeks of courses for graduate students, then a week of workshops in several areas of theoretical computer science. This program is particularly aimed at graduate students in mathematics, logic, theoretical computer science, mathematical linguistics and related areas. The program culminates in the 18th annual IEEE Logic in Computer Science (LICS2003) meeting on campus at U. Ottawa. For the latter, see http://www.dcs.ed.ac.uk/home/als/lics/ The details (and finances) of the Field's program are still being worked out, but we wanted to alert our colleagues to the following themes: Weeks 1,2: Each week will consist of two courses (one in the morning, the other in the afternoon), taught by experts in the area. We are planning topics that include: Week 1: (a) Categorical Logic and type theory and (b) Linear Logic. Week 2: (a) Game Semantics and (b) Concurrency. Week 3: Workshops. These include, among other topics, June 15-16: Quantum Programming Languages (Org: Peter Selinger), June 18-19: Mathematical Linguistics (Org: J. Lambek) There are currently two other workshops being planned. Some Limited Funding Scholarships will be made available to graduate students for attending the workshop. More details on how to apply will be made available soon. Meanwhile, interested students may contact any members of the local logic team to be alerted as news becomes available. Philip Scott (phil@site.uottawa.ca) Richard Blute (rblute@mathstat.uottawa.ca) Peter Selinger (selinger@mathstat.uottawa.ca) From rrosebru@mta.ca Wed Jan 8 15:45:16 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 08 Jan 2003 15:45:16 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18WM88-0006Ym-00 for categories-list@mta.ca; Wed, 08 Jan 2003 15:44:48 -0400 From: Martin Escardo MIME-Version: 1.0 Message-ID: <15899.65358.998738.42379@acws-0054.cs.bham.ac.uk> Date: Wed, 8 Jan 2003 10:37:02 +0000 To: categories@mta.ca Subject: categories: Re: thoughts arising from a letter of Lawvere In-Reply-To: <3E13DF3B.59E2@maths.usyd.edu.au> References: <3E13DF3B.59E2@maths.usyd.edu.au> X-Mailer: VM 6.89 under 21.1 (patch 14) "Cuyahoga Valley" XEmacs Lucid Content-Type: text/plain; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 10 I (and a colleague) wonder whether what Max Kelly is referring to is what Brian Day published in an incredibly concise way in pages 4-5 of the paper "A reflection theorem for closed categories", J. Pure Appl. Algebra 2 (1972), no. 1, 1--11. Max Kelly writes: > [...] > This is of course classical; but what Brian had is the following. There > is an evident functor f: Top --> Qu; just call A --> X allowable if it > is continuous. There is an equally evident functor > g: Qu --> Top; call a subset open if its characteristic function into > the Sierpinski space 2 lies in Qu. We have the adjunction g --| f. As > with any adjunction, we have an equivalence between the full subcategory > of Top where the counit is invertible and the full subcategory of Qu > where the unit is invertible. > > The subcategory of Top here, of course reflective in Top, is the > category of k-spaces, better called the "compactly-generated" spaces; it > is also a coreflective full subcategory of Qu. Others have noticed this > since and published it; but certainly subsequent to Brian's 1968 (I > think) Master's thesis. > [...] (We would also be interested in having a copy of the version of the paper "On quotients maps preserved by product and pullback" before the translation from category theory to topology (referred to in the deleted part of Kelly's message). Is that still available?) Martin Escardo From rrosebru@mta.ca Wed Jan 8 20:54:55 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 08 Jan 2003 20:54:55 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18WQvW-0000dO-00 for categories-list@mta.ca; Wed, 08 Jan 2003 20:52:06 -0400 Date: Wed, 8 Jan 2003 11:57:46 -0800 From: "David B. Benson" To: categories@mta.ca Subject: categories: Re: Category and Scheduling Theory Message-ID: <20030108195746.GB14957@kamiak.eecs.wsu.edu> References: Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.4i Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 11 On Tue, Jan 07, 2003 at 03:36:35PM +0100, Claus Gwiggner wrote: > is category theory a suited language to express "structure" in > scheduling or combinatorial optimisation problems ? Yes. See R. Bird \& O. de Moor, \emph{Algebra of Programming}, Prentice Hall Europe, 1997. Cheers, David -- Professor David B. Benson (509) 335-2706 School of EE and Computer Science (EME 102) (509) 335-3818 fax PO Box 642752, Washington State University office: Sloan 308 and 307 Pullman WA 99164-2752 U.S.A. dbenson@eecs.wsu.edu ---------------------------------------------------------------------------------- From rrosebru@mta.ca Wed Jan 8 20:54:55 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 08 Jan 2003 20:54:55 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18WQwJ-0000g0-00 for categories-list@mta.ca; Wed, 08 Jan 2003 20:52:55 -0400 Date: Wed, 8 Jan 2003 17:52:44 -0500 (EST) From: Oswald Wyler To: categories@mta.ca Subject: categories: Reference wanted Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 12 For a category E with finite limits, every morphism f:A\to B induces a pullback functor f^*:E/B\to E/A of slice categories, with a left adjoint given by u:a\to a' \mapsto u:fa\to fa'. It has been well known since the late 1960's that this left adjoint is comonadic, but who proved this, and where? From rrosebru@mta.ca Thu Jan 9 21:16:03 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 09 Jan 2003 21:16:03 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18Wndm-0001ZJ-00 for categories-list@mta.ca; Thu, 09 Jan 2003 21:07:18 -0400 Message-ID: From: "C.F.Townsend" To: "categories@mta.ca" Subject: categories: Naturality of a Change of Base Result Date: Thu, 9 Jan 2003 14:39:27 -0000 MIME-Version: 1.0 X-Mailer: Internet Mail Service (5.5.2653.19) Content-Type: text/plain; charset="iso-8859-1" Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 13 Given a geometric morphism n:E->F between Grothendieck toposes (over, say, Set) E is both an F-indexed category and a Set-indexed category. There is the following change of base result for any small (i.e. internal to Set) category C: - The category of F-indexed functors p^*C->E is equivalent to the category of Set-indexed functors C->E (where the first E is as an F-indexed cat and the second as a Set-indexed cat). (And p:F->Set.) Is there anything published/known as to the naturality of this equivalence? It is easy to see that it is natural in functors on C; but I also think (a) that it may be natural with respect to filtred cocontinuous functors between inductive completions of C and (b) between filtered cocontinuous functors on E. Thanks for any thoughts on this technical question, Regards, Christopher Townsend (Open University). From rrosebru@mta.ca Thu Jan 9 21:16:03 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 09 Jan 2003 21:16:03 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18Wnc9-0001Oy-00 for categories-list@mta.ca; Thu, 09 Jan 2003 21:05:37 -0400 Date: Thu, 9 Jan 2003 15:28:43 +0100 (MET) From: Taylor Paul Message-Id: <200301091428.h09EShMo006193@pianeta.di.unito.it> To: categories@mta.ca Subject: categories: hereditarily finite sets X-AntiVirus: Scanned for viruses by VirusFinder @2001-tecnici@di.unito.it - Email Clean X-SpamCheck: not spam (whitelisted), SpamAssassin (score=1.1, required 5.4, DOUBLE_CAPSWORD) Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 14 Galchin Vasili asked: > I would like to know if anybody is doing research on applying > category theory to hereditarily-finite sets, e.g. where an object is > a hereditarily set with some kind of structure to it and morphism > that preserves that structure. > Obviously, the subcategory of SET where objects are just hered. finite > sets and morphisms are functions between hered. finite sets is not > "interesting". Also, the case where an object is a hered. set together > with an endomorphism doesn't sound "interesting". I take it that you want to capture the WELL FOUNDED ELEMENT RELATION, and also the SUBSET RELATION, from set theory. You may be interested in 1. Gerhard Osius, "Categorical set theory: a characterisation of the category of sets", Journal of Pure and Applied Algebra 4 (1974) 79--119. 2. Peter Johnstone, "Topos Theory", Cambridge University Press, 1977, of which chapter 9 has a summary of Osius's work. 3. Andre Joyal & Ieke Moerdijk, "Algebraic Set Theory", LMS Lecture Notes 220, Cambridge University Press, 1995. 4. Paul Taylor, "Intuitionistic Sets and Ordinals", Journal of Symbolic Logic, 61 (1996) 705--744. 5. Paul Taylor, "Practical Foundations of Mathematics", Cambridge University Press, 1999, especially Sections 6.3, 6.7 and 9.5. http://www.dcs.qmul.ac.uk/~pt/Practical_Foundations Gerhard Osius's work was significant in 1974 as one of the ways in which it was shown that toposes do the same thing as set theory. In fact Osius's is, so far as I am aware, the only 1970s work that discusses *set* theory - Benabou, Joyal, Lawvere, Mitchell etc showed that toposes do the same thing as some form of *type* theory. Of course, it is the latter that mathematicians actually use when they claim to be using set theory as foundations. (See Section 2.2 of my book for a type-theoretic formulation of set theory as mathematicians actually use it.) Joyal and Moerdijk treat a model of set theory as a free algebra (within some larger world) for singleton and unions of specified size. If you are specifically interested in "finiteness" rather than the hereditary aspects in general, this might be the structure that you want (page 88). My JSL paper develops the notions of "transitive set" and "ordinal" in the sense of a carrier equipped with a binary relation with particular properties. Its style is therefore like order theory or other "ordinary" mathematics, since it attributes no ontological significance to the relation. It gives a version of Mostowski's theorem, in which the extensional quotient of a well founded relation is constructed as the quotient by an equivalent relation, and not (as you will find the in the set theory textbooks) using Replacement. In both Joyal--Moerdijk and my work, it is shown that *several* qualitatively different notions of ordinal arise intuitionistically. What remains of considerable interest (once we have agreed that set theory is wrong, wrong, wrong) is Osius's categorical notion of recursion. The equation f(x) = r( { f(y) | y in [=element_of] x } ) he writes as the (3=1, not 2=2) commutative square P(f) { y | y in x } P(X) ---------> P(A) ^ ^ | | | | | | | | | | r | | | | | | - | f v x X -------------> A which we may of course generalise to a "homomorphism" from any P-coalgebra to any P-algebra, where indeed P may be any functor instead of the covariant powerset functor. The coalgebra admits recursion by definition if there is exactly one such "homomorphism" to any algebra whatever. Osius showed that coalgebra homomorphisms, P(h) P(A) --------> P(B) | | | | | r | s | | | | v v A -----------> B capture the set-theoretic inclusion relation A------------------------> P(A) ^ | | | | | r | ----| | | | | | | m v H >---------> U >----------> A Suppose that, for any mono m, if the above diagram is a pullback, then m is in fact an isomorphism. The we say that r:PA->A is a WELL FOUNDED COALGEBRA. Sections 6.3 and 6.7 of the book give a sketch of the theory of well founded coalgebras, and the final section (9.5) shows how this categorical notion of ordinal can be used to define transfinite iterates of a functor (for example, internally in a topos) I have a long unfinished paper containing all of the details about well founded coalgebras. This shows how the various intuitionistic notions of ordinal (plus some new ones!) arise from considering the "lower sets" functor on Pos instead of the covariant powerset on Set. Besides the functor P and the underlying category, we can vary the class of maps that we call "monos". In its role in the above "broken pullback" diagram, this controls the logical strength of the induction scheme, ie the number of quantifiers that we allow in the definition of the predicates for which induction is applicable. However, for characterising the ordinals, the interesting variability is in the class of "monos" used to define EXTENSIONALITY. The full subcategory of extensional coalgebras (those for which r:PA >--> A is "mono") is closed under arbitrary limits in the category of well founded coalgebras and coalgebra homomorphisms. However, depending on the particular situation, we need the axiom of REPLACEMENT to construct the reflection (left adjoint to the inclusion). One day, I hope to use this to explore this frighteningly strong set theoretical principle categorically. Paul Taylor pt@di.unito.it www.di.unito.it/~pt PS I'm afraid this stuff took a back seat to Abstract Stone Duality. From rrosebru@mta.ca Fri Jan 10 11:44:13 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 10 Jan 2003 11:44:13 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18X1Gi-0005J4-00 for categories-list@mta.ca; Fri, 10 Jan 2003 11:40:24 -0400 Message-ID: <3E1E9154.8060901@bluewin.ch> Date: Fri, 10 Jan 2003 10:24:36 +0100 From: Krzysztof Worytkiewicz User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.0.1) Gecko/20020823 Netscape/7.0 X-Accept-Language: en-us, en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Re: Benabou manuscript Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 15 Carl Futia wrote >Are there other sources which offer a substantial discussion of profunctors? > > The lecture notes www.mathematik.tu-darmstadt.de/~streicher/FIBR/DiWo.ps.gz are an excellent source. Krzysztof From rrosebru@mta.ca Sat Jan 11 09:15:42 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 11 Jan 2003 09:15:42 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18XLNA-0006Qs-00 for categories-list@mta.ca; Sat, 11 Jan 2003 09:08:24 -0400 Date: Fri, 10 Jan 2003 15:25:29 -0400 (AST) From: Bob Rosebrugh To: categories Subject: categories: TAC Contents: Volume 10 Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 16 Here is the table of contents of Volume 10 and subscription information for the journal Theory and Applications of Categories. The Editors invite high quality submissions. The full table of contents is at www.tac.mta.ca/tac/ THEORY AND APPLICATIONS OF CATEGORIES ISSN 1201-561X Volume 10 - 2002 1. A survey of definitions of n-category Tom Leinster, 1-70 2. A homotopy double groupoid of a Hausdorff space Ronald Brown, Keith A. Hardie, Klaus Heiner Kamps, Timothy Porter, 71-93 3. Entity-relationship-attribute designs and sketches Michael Johnson, Robert Rosebrugh and R.J. Wood, 94-112 4. Homology of Lie algebras with $\Lambda/q\Lambda$ coefficients and exact sequences Emzar Khmaladze, 113-126 5. Exponentiability of perfect maps: four approaches Susan Niefield, 127-133 6. Coherence for Factorization Algebras Robert Rosebrugh and R.J. Wood, 134-147 7. More on injectivity in locally presentable categories J. Rosicky, J. Adamek and F. Borceux, 148-161 8. Colocalizations and their realizations as spectra Friedrich W. Bauer, 162-179 9. On some properties of pure morphisms of commutative rings Bachuki Mesablishvili, 180-186 10. Change of base, Cauchy completeness and reversibility Anna Labella and Vincent Schmitt, 187-219 11. Derived Operations in Goguen Categories Michael Winter, 220-247 12. Sober spaces and continuations Paul Taylor, 248-300 13. Subspaces in abstract Stone duality Paul Taylor, 301-368 14. Directed homotopy theory, II. Homotopy constructs Marco Grandis, 369-391 15. The cyclic spectrum of a Boolean flow John F. Kennison, 392-409 16. Simultaneously Reflective And Coreflective Subcategories of Presheaves Robert El Bashir and Jiri Velebil, 410-423 17. Entropic Hopf algebras and models of non-commutative logic Richard F. Blute, Francois Lamarche, Paul Ruet, 424-460 18. HSP subcategories of Eilenberg-Moore algebras Michael Barr, 461-468 19. Opmonoidal monads Paddy McCrudden, 469-485 20. A duality relative to a limit doctrine C. Centazzo and E.M. Vitale, 486-497 SUBSCRIPTION/ACCESS TO ARTICLES Subscribers to the journal receive abstracts of accepted papers by electronic mail. Compiled TeX (.dvi), Postscript and PDF files of the full articles are available by Web/ftp. To subscribe, send a request to tac@mta.ca, including your name and a postal address. The journal is free to individuals. From rrosebru@mta.ca Sat Jan 11 15:51:30 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 11 Jan 2003 15:51:30 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18XRbf-00043h-00 for categories-list@mta.ca; Sat, 11 Jan 2003 15:47:47 -0400 Date: Fri, 10 Jan 2003 22:29:32 +0100 (CET) From: Femke van Raamsdonk To: categories@mta.ca Subject: categories: RTA'03: last call for papers Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=X-UNKNOWN Content-Transfer-Encoding: QUOTED-PRINTABLE Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 17 *********************************** * * * RTA'03 LAST CALL FOR PAPERS * * * *********************************** http://www.dsic.upv.es/~rdp03/rta The 14th Int. Conf. on Rewriting Techniques and Applications (RTA'03) will be part of the Federated Conf. on Rewriting, Deduction and Programming (RDP'03). IMPORTANT DATES: Jan 15 2003: Deadline electronic submission of title+short abstract Jan 22 2003: Deadline electronic submission of papers Mar 15 2003: Notification of acceptance of papers Apr 7 2003: Deadline for final versions of accepted papers Jun 9-11 '03: Conference. RTA is the major forum for the presentation of research on all aspects of rewriting. Typical areas of interest include (but are not limited to): * APPLICATIONS: case studies; (rule-based) programming; symbolic and algebraic computation; theorem proving; system synthesis and verification; proof checking. * FOUNDATIONS: matching and unification; narrowing; completion techniques; strategies; constraint solving; explicit substitutions. * FRAMEWORKS: string, term, and graph rewriting; lambda-calculus and higher-order rewriting; proof nets; constrained rewriting/deduction; categorical and infinitary rewriting. * IMPLEMENTATION: compilation techniques; parallel execution; rewriting tools. * SEMANTICS: equational logic; rewriting logic. INVITED TALKS will be given at RTA'03 by: * David McAllester Toyota Technological Institute at Chicago Joint invited speaker with TLCA * Jean-Louis Giavitto Universit=E9 d'Evry, France * Pat Lincoln SRI International BEST PAPER AWARDS: A 1000 Euro award wil be given to the best paper or papers as decided by the PC. The award may also totally or partially go to the best paper with a student as main author, according to the submission letter. RTA'03 PROGRAM COMMITEE: * Harald Ganzinger (Max-Planck-Institut) * Claude Kirchner (Nancy) * Salvador Lucas (Valencia) * Chris Lynch (Clarkson) * Jos=E9 Meseguer (Urbana) * Robert Nieuwenhuis (Barcelona, Chair) * Tobias Nipkow (Munich) * Vincent van Oostrom (Utrecht) * Christine Paulin (Paris-sud) * Frank Pfenning (Carnegie Mellon) * Mario Rodr=EDguez-Artalejo (Madrid) * Sophie Tison (Lille) * Ashish Tiwari (SRI) * Andrei Voronkov (Manchester) * Hantao Zhang (Iowa) RTA'03 SUBMISSIONS: Submissions must be original and not submitted for publication elsewhere. Submission categories include regular research papers and system descriptions. Also problem sets and submissions decribing interesting applications of rewriting techniques will be very welcome. As usual, accepted papers will appear in the Springer-Verlag Lecture Notes in Computer Science series. See the RDP'03 web page for details. For further questions please contact the program chair: RTA'03 PROGRAM CHAIR: Robert Nieuwenhuis Technical University of Catalonia Jordi Girona 1, E-08034 Barcelona, Spain roberto@lsi.upc.es From rrosebru@mta.ca Sat Jan 11 15:51:30 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 11 Jan 2003 15:51:30 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18XRcS-00045N-00 for categories-list@mta.ca; Sat, 11 Jan 2003 15:48:36 -0400 X-Authentication-Warning: triples.math.mcgill.ca: barr owned process doing -bs Date: Sat, 11 Jan 2003 11:48:56 -0500 (EST) From: Michael Barr To: Categories list Subject: categories: Recoltes et Semailles Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 18 I call your attention to the existence of the beginnings of an English translation of Grothendieck's Memoirs, Recoltes et Semailles (which, IMHO ought to be translated as Reapings and Sowings): http://www.fermentmagazine.org/Grothendieck/recoltes1.html Michael From rrosebru@mta.ca Sat Jan 11 16:13:58 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 11 Jan 2003 16:13:58 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18XRzy-0005Q4-00 for categories-list@mta.ca; Sat, 11 Jan 2003 16:12:54 -0400 Message-Id: <200301090403.h0943Vc11733@math-cl-n01.ucr.edu> Subject: categories: 2-category of internal categories To: categories@mta.ca (categories) Date: Wed, 8 Jan 2003 20:03:31 -0800 (PST) From: "John Baez" X-Mailer: ELM [version 2.5 PL6] MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 19 Dear Categorists - Who first constructed internal categories, internal functors and internal natural transformations in a given category, and actually proved that these form a *2-category*? I'm looking for a reference. Best, jb From rrosebru@mta.ca Mon Jan 13 20:09:53 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 13 Jan 2003 20:09:53 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18YEWY-0002Tb-00 for categories-list@mta.ca; Mon, 13 Jan 2003 20:01:46 -0400 Message-ID: <3E207C72.19A59B5F@member.ams.org> Date: Sat, 11 Jan 2003 21:20:02 +0100 From: Pasha Zusmanovich Organization: Home X-Mailer: Mozilla 4.77 [en] (X11; U; Linux 2.4.5 i686) X-Accept-Language: en MIME-Version: 1.0 To: Categories list Subject: categories: Re: Recoltes et Semailles References: Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 20 Michael Barr wrote: > > I call your attention to the existence of the beginnings of an English > translation of Grothendieck's Memoirs, Recoltes et Semailles (which, IMHO > ought to be translated as Reapings and Sowings): > > http://www.fermentmagazine.org/Grothendieck/recoltes1.html > > Michael Though the following is of much less broad interest, I think it is appropriate to be noticed. There is a (full) Russian translation, available both online (at http://www.mccme.ru/free-books/) and as a published book. -- Met vriendlijke groet(je), Pasha http://www.justpasha.org/ From rrosebru@mta.ca Mon Jan 13 20:09:53 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 13 Jan 2003 20:09:53 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18YEZ9-0002gg-00 for categories-list@mta.ca; Mon, 13 Jan 2003 20:04:27 -0400 From: "NASSLLI'03 Bloomington, Indiana" X-Sender: nasslli@lear.ucs.indiana.edu To: Undisclosed recipients: ; Subject: categories: NASSLLI-2003. Student Session Call for Papers. Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Date: Mon, 13 Jan 2003 20:04:27 -0400 Status: RO X-Status: X-Keywords: X-UID: 21 C a l l f o r P a p e r s NASSLLI-2003 Second North American Summer School in Logic, Language, and Information http://www.indiana.edu/~nasslli/ June 17-21, 2003, Bloomington, Indiana NASSLLI '02 Continues North American Summer School Tradition --------- Following last year's founding of a North American counterpart to the European Summer School for Logic, Language and Information, this year's NASSLLI will be at Indiana University. It will again feature a Student Session where students can network and get feedback on their work -- both from faculty and student attendees. This CFP solicits submissions to the student session. Topics of Interest ------- The areas of interest are Logic -- including work on problems of mathematical or philosophical interest Language -- including descriptive or theoretical work in formal linguistics Language and Logic -- applications of logic to natural language Language and Computation -- theoretical and empirical work in computational linguistics Logic and Computation -- automated theorem-proving and related fields Computation -- artificial intelligence or related areas of computer science Work integrating several of these areas is of particular interest. Requirements ----- The Student Session papers should describe original, unpublished work that has been completed. However, no previously published papers should be submitted. All authors must be at the pre-doctoral level; submissions co-authored by non-students will be discarded. Format of Submission ----- Full papers, not to exceed 10 pages, are to be submitted by email as Adobe Portable Document Files (PDF). This file must include a separate identification page including the following pieces of information: Title: title of the submission First author: firstname lastname Address: address of the first author ...... Last author: firstname lastname Address: address of the last author Short summary: abstract (5 lines) Subject area (one or two of): Logic | Language | Computation Other Conferences Submitted To: Neither this identification page, nor any bibliography counts towards the 10 page limit. Since reviewing will be blind, the body of the paper should omit author names and addresses. Furthermore, self-references that reveal the author's identity (e.g., "We previously showed (Smith, 1991)... ") should be avoided. It is possible to use instead references like "Smith (1991) previously showed..." The PDF of the paper is to be enclosed in an email duplicating the information on the identification page. Use US Letter paper and LaTeX if possible; accepted papers will need to be resubmitted without page numbers. Please email submissions to John Hale by MARCH 15th 2003. NASSLLI '03 ----- At least one author needs to register for NASSLLI '03 in order to be in the student session. Accepted papers will be available at the Summer School in the Student Session Proceedings (tentative plans exist for on-line dissemination as well). One of the authors will give a 20-minute talk with up to 10 minutes for discussion. Dates ---- Deadline for submission of papers : March 15th, 2003 Author notifications : May 1st, 2003 Revisions in accepted papers due by : June 1st, 2003 ESSLLI-2003 Student Session : June 17-21, 2003. Confirmed Student Session Program Committee Members ---- Julia Hockenmaier, University of Edinburgh Gerhard Jaeger, Potsdam University Greg Kobele, UCLA Yevgeniy Makarov, Indiana University Gideon Mann, Johns Hopkins University Jens Michaelis, Potsdam University Rachel Sussman, University of Rochester Please direct any questions about the NASSLI-03 student session to John Hale . From rrosebru@mta.ca Mon Jan 13 20:09:53 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 13 Jan 2003 20:09:53 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18YEXV-0002Zp-00 for categories-list@mta.ca; Mon, 13 Jan 2003 20:02:45 -0400 From: maxk@maths.usyd.edu.au (Max Kelly) Message-Id: <200301120527.h0C5Ruq312044@milan.maths.usyd.edu.au> To: categories@mta.ca Subject: categories: Re: 2-category of internal categories Sender: cat-dist@mta.ca Precedence: bulk Date: Mon, 13 Jan 2003 20:02:45 -0400 Status: RO X-Status: X-Keywords: X-UID: 22 John Baez asks who constructed internal categories, functors, and natural transformations, proving these to form a 2-category; and seeks a reference. The answer is surely Ehresmann; and the precise reference must be in an early part of his collected works, produced after his death, with a detailed commentary, by his widow Andree Ehresmann-Bastiani. I have at least the earlier volumes of these, which - being now a visitor here in Sydney, John - you may certainly borrow. I'll have a bit of a look myself, if I have the time; Ehresmann's language is at times far from what has now become the norm. (Finding his categorical insights into differential geometry unappreciated by his French colleagues, he cut himself off and set up an independent group based in Paris VI (where he was) and in Amiens (where Bastiani was); with their own journal, Cahiers de Topologie et Geometrie Differentialle. The definitive rapprochement between this group and other category theorists dates from 1973, when the first of several international conferences at Amiens was arranged by Ehresmann and Bastiani.) Probably there will be no need for me to take these volumes down tonight; for Andree will doubtless see John's question when it dawns in Paris in an hour or two, and will doubtless give us chapter and verse. Max Kelly. From rrosebru@mta.ca Mon Jan 13 20:09:53 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 13 Jan 2003 20:09:53 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18YEb7-0002mp-00 for categories-list@mta.ca; Mon, 13 Jan 2003 20:06:29 -0400 Message-ID: <3E226E6F.167E@maths.usyd.edu.au> Date: Mon, 13 Jan 2003 18:44:47 +1100 From: Max Kelly Organization: School of Mathematics and Statistics, University of Sydney X-Mailer: Mozilla 3.01Gold (X11; I; OSF1 V5.1 alpha) MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Re: thoughts arising from a letter of Lawvere References: <3E13DF3B.59E2@maths.usyd.edu.au> <15899.65358.998738.42379@acws-0054.cs.bham.ac.uk> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 23 Martin Escardo (Categories 8 Jan.) is correct in surmising that the results of Brian Day's 1968 M.Sc. thesis are included, in a much more general form, as an example in his 1972 article in JPAA. My point was only the history of the matter; the 1972 paper is one of three which together expound the content of Brian's Ph.D. thesis, and appeared four years later than his Masters degree. In the interim the adjunction between topological spaces and Spanier's quasi-spaces, and the relation of this to compactly-generated spaces, had been observed and published by two or three other of our colleagues; Booth was one, and there was at least one more whose name escapes me. Brian was then rueful about not submitting the M.Sc. thesis for publication in 1968; as his supervisor, I shared his rue. Martin also seeks more information about the hidden category theory behind my 1970 paper with Brian. There was never anything like a "categorical version" that got turned into a "topological" one; we translated as we went. I believe my 2 Jan. letter to Categories contains enough hints to make a reconstruction straightforward, even if a bit long and tedious. Max Kelly. From rrosebru@mta.ca Mon Jan 13 20:09:53 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 13 Jan 2003 20:09:53 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18YEYJ-0002ei-00 for categories-list@mta.ca; Mon, 13 Jan 2003 20:03:35 -0400 Date: Sun, 12 Jan 2003 15:46:49 -0500 (EST) From: Foundations of Computing Message-Id: <200301122046.h0CKknx05451@moose.cs.indiana.edu> To: categories@mta.ca Subject: categories: jobs: CS Theory positions Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 24 [Sincere apologies for multiple copies] FACULTY POSITIONS IN ALGORITHMS AND CS THEORY ============================================= Indiana University's Computer Science Department is conducting a broad faculty search. That effort has recently been expanded to INCLUDE POSITIONS IN ALL AREAS OF THEORETICAL COMPUTER SCIENCE. For detail see www.cs.indiana.edu/Contacts/employment. For additional information please see www.cs.indiana.edu/foundations/foc www.indiana.edu/~iulg From rrosebru@mta.ca Mon Jan 13 20:33:17 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 13 Jan 2003 20:33:17 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18YF05-0004X2-00 for categories-list@mta.ca; Mon, 13 Jan 2003 20:32:17 -0400 Message-Id: <5.1.0.14.1.20030113192144.009f1cb0@mailx.u-picardie.fr> X-Sender: ehres@mailx.u-picardie.fr X-Mailer: QUALCOMM Windows Eudora Version 5.1 Date: Mon, 13 Jan 2003 19:22:21 +0100 To: categories@mta.ca From: Andree Ehresmann Subject: categories: In answer to John Baez Mime-Version: 1.0 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 25 In answer to John Baez Charles Ehresmann introduced internal categories to unify several examples of this notion that he had studied in earlier papers, namely topological and differentiable categories and specially groupoids (i.e. internal to Top and Diff) which he used extensively in his works on the foundations of differential geometry in the early fifties, ordered categories of several types (i.e. internal to sub-categories of the category of posets) also used in these works, and double categories (of which the 2-categories are a particular case) which he had introduced in his 1958 paper "Categorie des foncteurs types", Rev. Un. Mat. Argentina XX (1960). He defines the notion of internal categories (which he called "categorie structuree") and internal functors in the paper "Categories structurees", Ann. Ec. Normale Sup. 80 (1963), and internal natural transformations in the sequel of this paper "Categories structurees III: Quintettes et applications covariantes", Cahiers Top. et GD V (1963) where he constructs the double category of "quintettes structures" of which the 2-category of internal categories is a sub-2-category. However in these papers he defined only categories internal to a concrete category, which explains the name "categorie structuree". Later on he defined the general notion of an internal category, initially called "categorie structuree generalisee", in "Introduction to the theory of structured categories", Technical Report 10, Un. of Kansas at Lawrence, 1966 where he introduced the theory of sketches and, in particular, the sketch of a category. In this paper and in the paper "Categories structurees generalisees", Cahiers de Top. et GD X-1 (1968) he compares with the notion of a "C-category on (A,A0)" which Grothendieck had defined in 1960-61 by the fact that the Hom(A,-) are equipped with a natural strucutre of category. All the papers of Charles are reprinted in "Charles Ehresmann: Oeuvres completes et commentees", in the comments of which I give more historical information on this subject.. With all my best wishes for 2003 Andree C. Ehresmann From rrosebru@mta.ca Tue Jan 14 20:47:01 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 14 Jan 2003 20:47:01 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18YbYz-0002Lb-00 for categories-list@mta.ca; Tue, 14 Jan 2003 20:37:49 -0400 Mime-Version: 1.0 X-Sender: street@hera.ics.mq.edu.au Message-Id: In-Reply-To: <3E226E6F.167E@maths.usyd.edu.au> Date: Tue, 14 Jan 2003 11:30:29 +1100 To: categories@mta.ca From: Ross Street Subject: categories: Re: thoughts arising from a letter of Lawvere Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 26 Sammy Eilenberg told me he wrote a paper based on the Day-Kelly paper On topological quotient maps preserved by pullbacks or products, Proc. Cambridge Phil. Soc. 67 (1970) 553-558. I believe Sammy's paper was for an MAA expository series. It sounded a beautiful approach but I did not see the manuscript and forget the details. While the paper was in the universal categorical spirit it made only one parenthetic remark that something was a category. Sammy claimed this was why the paper was rejected. What a great pity! I would love to have a copy of the preprint. Does anyone else know about it? --Ross From rrosebru@mta.ca Wed Jan 15 14:16:55 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 15 Jan 2003 14:16:55 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18Ys0y-0007MC-00 for categories-list@mta.ca; Wed, 15 Jan 2003 14:11:48 -0400 Date: Tue, 14 Jan 2003 16:31:07 +0100 To: categories@mta.ca Subject: categories: ETAPS 2003 - call for participation Message-Id: <20030114153107.66E73592D@duch.mimuw.edu.pl> From: etaps03@mimuw.edu.pl (Konferencja ETAPS'03) X-Virus-Scanned: by amavisd-new Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 27 We apologize if you receive multiple copies of this message. ********************************************************** *** *** *** ETAPS 2003 *** *** Warsaw, Poland, April, 5-13, 2003 *** *** *** *** CALL FOR PARTICIPATION *** *** *** *** !!!! REGISTER NOW !!!! *** *** *** *** http://www.mimuw.edu.pl/etaps03/ *** *** *** ********************************************************** ********************************************************** *** *** *** Important Dates *** *** *** *** January 31 - Grant Application Deadline *** *** February 5 - Discount Registration Deadline *** *** March 3 - Early Registration Deadline *** *** March 31 - End of Online Registration *** *** *** *** April 5-13 - ETAPS 03 *** *** *** ********************************************************** ----------------------------------------------------------------------- 5 Conferences - 15 Workshops - 7 Tutorials ----------------------------------------------------------------------- The European Joint Conferences on Theory and Practice of Software (ETAPS) is the primary European forum for academic and industrial researchers working on topics related to Software Science. It is a confederation of five main conferences, a number of satellite workshops and other events. ----------------------------------------------------------------------- Conferences ----------------------------------------------------------------------- CC 2003: International Conference on Compiler Construction http://www.cs.lth.se/~gorel/cc03/ Chair: Gorel Hedin (Lund, Sweden), gorel@cs.lth.se ESOP 2003, European Symposium on Programming http://www.di.unipi.it/ESOP03/ Chair: Pierpaolo Degano (Pisa, Italy), degano@di.unipi.it FASE 2003, Fundamental Approaches to Software Engineering http://www.lta.disco.unimib.it/fase2003/ Chair: Mauro Pezz`e (Italy), pezze@disco.unimib.it FOSSACS 2003 Foundations of Software Science and Computation Structures http://research.microsoft.com/~adg/FOSSACS03/ Chair: Andrew Gordon (Microsoft Research, UK), adg@microsoft.com TACAS 2003, Tools and Algorithms for the Construction and Analysis of Systems ttp://www.inrialpes.fr/vasy/tacas03/ Co-Chairs: Hubert Garavel (INRIA, France), Hubert.Garavel@inria.fr John Hatcliff (Kansas State, USA), hatcliff@cis.ksu.edu ----------------------------------------------------------------------- Invited Speakers: ----------------------------------------------------------------------- Samson Abramsky, Oxford University, UK Tony Hoare, Microsoft Research, Cambridge, UK Peter Lee, Carnegie Mellon University, USA Xavier Leroy, INRIA and Trusted Logic, France Catherine Meadows, Naval Research Laboratory, USA Barbara Ryder, Rutgers University, USA Michal Young, Oregon University, USA ----------------------------------------------------------------------- Workshops ----------------------------------------------------------------------- SE-WMT = Structured Programming: The Hard Core of Software Engineering (special event to honour Prof. W.M.Turski's 65th birthday) AVIS = Automated Verification of Infinite-State Systems CMCS = Coalgebraic Methods in Computer Science COCV = Compiler Optimization Meets Compiler Verification Feyerabend = Feyerabend - Redefining Computing FAMAS = Formal Approaches to Multi-Agent Systems FICS = Fixed Points in Computer Science LDTA = Language Description, Tools and Applications RSKD = Rough Sets in Knowledge Discovery and Soft Computing SC = Software Composition TACoS = Test and Analysis of Component Based Systems USE = Unanticipated Software Evolution UniGra = Uniform Approaches to Graphical Specification Techniques WITS = Workshop on Issues in the Theory of Security WOOD = Workshop on Object-Oriented Developments ----------------------------------------------------------------------- Tutorials ----------------------------------------------------------------------- + Foundations of Constraint Programming + XML Documents Using Tree Automata + Multi-Media Instruction in Safe and Secure Systems + Advanced Compilation Techniques for the Itanium Processor Family + Formal Development of Critical Systems with UML + An Inside Look at Rotor, Microsoft's "Shared Source" Implementation of the Common Language Infrastructure + Theory and Practice of Co-Verification Process: UniTesk Story ********************************************************** *** *** *** More information and registration form at *** *** *** *** www.mimuw.edu.pl/etaps03 *** *** *** *** !!!! REGISTER NOW !!!! *** *** *** ********************************************************** ----------- you received this e-mail via the individual or collective address categories@mta.ca to unsubscribe from ETAPS list: contact etaps03@mimuw.edu.pl ----------- From rrosebru@mta.ca Wed Jan 15 15:03:04 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 15 Jan 2003 15:03:04 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18Ysn5-0002v1-00 for categories-list@mta.ca; Wed, 15 Jan 2003 15:01:31 -0400 Message-ID: <3E256980.AEFD39A1@csc.liv.ac.uk> Date: Wed, 15 Jan 2003 14:00:32 +0000 From: Peter McBurney X-Mailer: Mozilla 4.79 [en] (X11; U; Linux 2.4.18-10 i686) X-Accept-Language: en MIME-Version: 1.0 To: CATEGORIES LIST Subject: categories: Generalization of Browder's F.P. Theorem? Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 28 Hello -- Does anyone know of a generalization of Browder's Fixed Point Theorem from R^n to arbitrary topological spaces, or to categories of same? ***************** Theorem (Browder, 1960): Suppose that S is a non-empty, compact, convex subset of R^n, and let f: [0,1] x S --> S be a continuous function. Then the set of fixed points { (x,s) | s = f(x,s), x \in [0,1] and s \in S } contains a connected subset A such that the intersection of A with {0} x S is non-empty and the intersection of A with {1} x S is non-empty. ***************** Many thanks, -- Peter McBurney University of Liverpool, UK From rrosebru@mta.ca Thu Jan 16 18:08:41 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 16 Jan 2003 18:08:41 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18ZI41-0002Hw-00 for categories-list@mta.ca; Thu, 16 Jan 2003 18:00:41 -0400 Message-ID: <3E26BBF3.2D413C6A@cs.bham.ac.uk> Date: Thu, 16 Jan 2003 14:04:35 +0000 From: Steven J Vickers Organization: School of Computer Science, The University of Birmingham, U.K. X-Mailer: Mozilla 4.79 [en] (X11; U; Linux 2.4.18-5 i686) X-Accept-Language: en MIME-Version: 1.0 To: CATEGORIES LIST CC: Peter McBurney Subject: categories: Re: Generalization of Browder's F.P. Theorem? References: <3E256980.AEFD39A1@csc.liv.ac.uk> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 29 I'm intrigued by Peter McBurney's question [below]. It looks rather like a question of the constructive content of Brouwer's fixed point theorem. Suppose S is (homeomorphic to) an n-cell. Then in the internal logic of the topos of sheaves over [0,1], f is just a continuous endomap of S. If Brouwer's theorem were constructively true then f would have a fixpoint, and that would come out as a continuous section of the projection [0,1]xS -> [0,1]. More precisely, it would be a map g: [0,1] -> S such that f(x, g(x)) = g(x) for all x. If this existed then the set A = {(x, g(x))| x in [0,1]} would be as required. However, the proof of Brouwer that I've seen is not constructive - it goes by contradiction. So maybe the requirements on A are a way of getting constructive content in Brouwer's result. What is known constructively about Brouwer's fixed point theorem? Steve Vickers. Peter McBurney wrote: > Hello -- > > Does anyone know of a generalization of Browder's Fixed Point Theorem > from R^n to arbitrary topological spaces, or to categories of same? > > ***************** > > Theorem (Browder, 1960): Suppose that S is a non-empty, compact, convex > subset of R^n, and let > > f: [0,1] x S --> S > > be a continuous function. Then the set of fixed points > > { (x,s) | s = f(x,s), x \in [0,1] and s \in S } > > contains a connected subset A such that the intersection of A with {0} x > S is non-empty and the intersection of A with {1} x S is non-empty. > > ***************** > > Many thanks, > > -- Peter McBurney > University of Liverpool, UK From rrosebru@mta.ca Fri Jan 17 11:43:39 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 17 Jan 2003 11:43:39 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18ZYbR-0005iS-00 for categories-list@mta.ca; Fri, 17 Jan 2003 11:40:17 -0400 Date: Thu, 16 Jan 2003 23:00:44 +0000 (GMT) From: "Prof. Peter Johnstone" To: CATEGORIES LIST , Subject: categories: Re: Generalization of Browder's F.P. Theorem? In-Reply-To: <3E26BBF3.2D413C6A@cs.bham.ac.uk> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Scanner: exiscan for exim4 (http://duncanthrax.net/exiscan/) *18ZJ0C-0005sw-00*vyUCLebRbnw* Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 30 On Thu, 16 Jan 2003, Steven J Vickers wrote: > > I'm intrigued by Peter McBurney's question [below]. It looks rather like a > question of the constructive content of Brouwer's fixed point theorem. > > Suppose S is (homeomorphic to) an n-cell. Then in the internal logic of the > topos of sheaves over [0,1], f is just a continuous endomap of S. If > Brouwer's theorem were constructively true then f would have a fixpoint, > and that would come out as a continuous section of the projection [0,1]xS > -> [0,1]. More precisely, it would be a map g: [0,1] -> S such that f(x, > g(x)) = g(x) for all x. If this existed then the set A = {(x, g(x))| x in > [0,1]} would be as required. > > However, the proof of Brouwer that I've seen is not constructive - it goes > by contradiction. So maybe the requirements on A are a way of getting > constructive content in Brouwer's result. > > What is known constructively about Brouwer's fixed point theorem? > > Steve Vickers. > Similar thoughts had occurred to me. Brouwer's theorem is clearly not constructive, since it doesn't hold (even locally) continuously in parameters (consider a path in the space of endomaps of [0,1] passing through the identity, where the fixed point `flips' from one end of the interval to the other as it does so). However, Browder's result would seem to suggest that the `locale of fixed points of f' (that is, the equalizer of f and the identity in the category of locales) might be consistent (that is, `inhabited') in general, even though it may not have any points. It's certainly conceivable that that might be true constructively, though I can't see how to prove it -- but it isn't the full content of Browder's theorem. Peter Johnstone From rrosebru@mta.ca Fri Jan 17 11:43:40 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 17 Jan 2003 11:43:40 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18ZYcr-0005np-00 for categories-list@mta.ca; Fri, 17 Jan 2003 11:41:45 -0400 X-Authentication-Warning: triples.math.mcgill.ca: barr owned process doing -bs Date: Thu, 16 Jan 2003 18:05:39 -0500 (EST) From: Michael Barr X-Sender: barr@triples.math.mcgill.ca To: CATEGORIES LIST , Subject: categories: Re: Generalization of Browder's F.P. Theorem? In-Reply-To: <3E26BBF3.2D413C6A@cs.bham.ac.uk> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 31 In Errett Bishop's Constructive Analysis (anyone who is interested in analysis over a topos absolutely must know this book), he proves that for any continuous endomorphism f of a disk and for every eps > 0, there is a point x in the disk for which |f(x) - x| < eps. A couple of points should be made. First f has to be constructible and eps has to be provably positive. For Bishop, a real number is an equivalence class of pairs of RE sequences of integers a_n and b_n such that for all m,n |a_n/b_n - a_m/b_m| < 1/m + 1/n and a function is constructive if it is a machine for turning one such sequence into another. To be continuous, it there must be a function delta(eps) that produces for each eps > 0, a delta(eps) such that |x - y| < delta(eps) implies that |f(x) - f(y)| < eps. (In fact, there is a non-constructive proof that every constructive function is continuous.) Bishop then claims, without proof as far as I can see, that there is a fixed point free endomorphism of the disk. What this means is that when you extend this function to all reals, any fixed point is not a constructible real number. On Thu, 16 Jan 2003, Steven J Vickers wrote: > > I'm intrigued by Peter McBurney's question [below]. It looks rather like a > question of the constructive content of Brouwer's fixed point theorem. > > Suppose S is (homeomorphic to) an n-cell. Then in the internal logic of the > topos of sheaves over [0,1], f is just a continuous endomap of S. If > Brouwer's theorem were constructively true then f would have a fixpoint, > and that would come out as a continuous section of the projection [0,1]xS > -> [0,1]. More precisely, it would be a map g: [0,1] -> S such that f(x, > g(x)) = g(x) for all x. If this existed then the set A = {(x, g(x))| x in > [0,1]} would be as required. > > However, the proof of Brouwer that I've seen is not constructive - it goes > by contradiction. So maybe the requirements on A are a way of getting > constructive content in Brouwer's result. > > What is known constructively about Brouwer's fixed point theorem? > > Steve Vickers. > > Peter McBurney wrote: > > > Hello -- > > > > Does anyone know of a generalization of Browder's Fixed Point Theorem > > from R^n to arbitrary topological spaces, or to categories of same? > > > > ***************** > > > > Theorem (Browder, 1960): Suppose that S is a non-empty, compact, convex > > subset of R^n, and let > > > > f: [0,1] x S --> S > > > > be a continuous function. Then the set of fixed points > > > > { (x,s) | s = f(x,s), x \in [0,1] and s \in S } > > > > contains a connected subset A such that the intersection of A with {0} x > > S is non-empty and the intersection of A with {1} x S is non-empty. > > > > ***************** > > > > Many thanks, > > > > -- Peter McBurney > > University of Liverpool, UK > > > > From rrosebru@mta.ca Fri Jan 17 11:56:08 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 17 Jan 2003 11:56:08 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18ZYqF-0006pA-00 for categories-list@mta.ca; Fri, 17 Jan 2003 11:55:35 -0400 From: Xindong Wu Message-Id: <200301161917.h0GJHv024228@kais.emba.uvm.edu> Subject: categories: job: Dorothean Professor in CS at U Vermont (Applications by 1/20/03) To: categories@mta.ca Date: Thu, 16 Jan 2003 14:17:57 -0500 (EST) X-Mailer: ELM [version 2.5 PL2] MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 32 Dorothean Professor in Computer Science at the University of Vermont ==================================================================== Applications (either hardcopy or by e-mail) by January 20, 2003 *************************************************************** The College of Engineering and Mathematics at the University of Vermont invites applications for the Dorothean Professorship (at the Full Professor or Associate Professor level) in Computer Science, commencing with the 2003-04 academic year. Tenure will be sought at time of appointment. The University of Vermont, one of the top public national universities, is located in Burlington, Vermont. It offers a supportive research environment in a relatively small city that repeatedly has drawn national attention for offering a high quality of life. The greater Burlington area includes 125,000 people, and is situated on the shores of Lake Champlain between the Green Mountains of Vermont and the Adirondack Mountains of New York. Burlington and the surrounding area provide an environment rich in cultural and recreational activities. The Department of Computer Science offers programs in the College of Engineering and Mathematics and the College of Arts and Sciences, as well as a joint program with the School of Business Administration. Our existing faculty in Computer Science are involved in the forefront of research in knowledge and data engineering (such as data mining, database systems, pattern recognition, and knowledge-based systems), software engineering and verification (including programming languages), and computational sciences (including computational biology, discrete modeling, and numerical methods). We are seeking to complement and further strengthen our existing research and teaching activities in these areas. Candidates in these areas are most sought, and candidates in any other area of computer science will also be considered seriously. Candidates should have a distinguished research record, hold a doctorate in Computer Science or a closely related field, and have broad teaching abilities and interests. The successful applicant is expected to (1) play a major role in departmental research initiatives and the graduate program coordination, (2) strengthen and build interdisciplinary bridges between the Department of Computer Science and other departments within the University, and (3) take an active role in teaching computer science courses. Please send a letter of interest, a curriculum vitae, a statement of teaching experience and interests, a statement of research interests and aspirations to, and arrange for at least three letters of reference to be sent to Chair, Dorothean Professor Search Committee, Department of Computer Science, University of Vermont, Burlington, VT 05405. Complete applications received by January 20, 2003 will be fully considered. For more information about the Department and the College please see http://www.cs.uvm.edu or email to cssearch@emba.uvm.edu. The University of Vermont is an Affirmative Action/Equal Opportunity employer and encourages applications from women and members of minority groups. From rrosebru@mta.ca Fri Jan 17 13:55:43 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 17 Jan 2003 13:55:43 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18ZagH-0007bk-00 for categories-list@mta.ca; Fri, 17 Jan 2003 13:53:25 -0400 From: Carl Futia Message-ID: <18b.14dc2e08.2b59872b@aol.com> Date: Fri, 17 Jan 2003 11:19:55 EST Subject: categories: Re: Generalization of Browder's F.P. Theorem? To: categories@mta.ca MIME-Version: 1.0 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 33 There seems to be some confusion about the theorem Peter McBurney asked about. The reference he cited was by Felix E. BROWDER (1960) who proved a number of fixed point results of considerable interest to functional analysts. The theorem the list seems to be discussing is due to BROUWER (Math. Ann. 69(1910) and 71(1912). Carl Futia From rrosebru@mta.ca Sat Jan 18 09:23:01 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 18 Jan 2003 09:23:01 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18Zsoz-0002uv-00 for categories-list@mta.ca; Sat, 18 Jan 2003 09:15:37 -0400 Message-Id: <3.0.5.32.20030118123942.008242a0@mailhost.cs.bham.ac.uk> X-Sender: sjv@mailhost.cs.bham.ac.uk X-Mailer: QUALCOMM Windows Eudora Light Version 3.0.5 (32) Date: Sat, 18 Jan 2003 12:39:42 +0000 To: categories@mta.ca From: S Vickers Subject: categories: Re: Generalization of Browder's F.P. Theorem? In-Reply-To: <18b.14dc2e08.2b59872b@aol.com> Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 34 At 11:19 17/01/03 EST, you wrote: >There seems to be some confusion about the theorem Peter McBurney asked about. > >The reference he cited was by Felix E. BROWDER (1960) who proved a number of >fixed point results of considerable interest to functional analysts. > >The theorem the list seems to be discussing is due to BROUWER (Math. Ann. >69(1910) and 71(1912). > >Carl Futia No, there is no confusion. Browder's theorem appears to provide insight into the constructive content of Brouwer's theorem. Both are being discussed. Steve Vickers. From rrosebru@mta.ca Tue Jan 21 19:21:02 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 21 Jan 2003 19:21:02 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18b7bZ-0003QS-00 for categories-list@mta.ca; Tue, 21 Jan 2003 19:14:53 -0400 To: CATEGORIES LIST Subject: categories: Re: Generalization of Browder's F.P. Theorem? References: Reply-To: Andrej Bauer From: Andrej Bauer Date: 21 Jan 2003 19:11:24 +0100 In-Reply-To: Michael Barr's message of "Thu, 16 Jan 2003 18:05:39 -0500 (EST)" Message-ID: Lines: 48 User-Agent: Gnus/5.0807 (Gnus v5.8.7) XEmacs/21.4 (Common Lisp) MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 35 Michael Barr writes: > For Bishop, a real number is an equivalence class of pairs of > RE sequences of integers a_n and b_n such that for all m,n |a_n/b_n - > a_m/b_m| < 1/m + 1/n ... Actually, Bishop purposely avoids taking a real to be an equivalence class of sequences, presumably because he does not want to assume the axiom of countable choice. A sequence as described above is sometimes called a "fundamental sequence". Two such sequences x = (a_n/b_n) and y = (c_n/b_n) are said to "coincide", written x ~ y iff |a_n/b_n - c_m/d_m| < 2/n + 2/m, where I might have gotten the right-hand side slightly wrong. Now there are two possibilities: (1) we say that a real is an equivalence class of fundamental sequences under the relation ~, or (2) we say that a real _is_ a fundamental sequence, where two reals are claimed "equal" if they coincide (the approach taken by Bishop). The first alternative gives us what is usually called "Cauchy reals". The difference between the two is apparent when we attempt to show that every Cauchy sequence of reals has a limit. In the first case we are given a sequence of equivalence classes of fundamental sequences. In order to construct a fundamental sequence representing the limit we need to _choose_ a representative from each equivalence class. In the second case a Cauchy sequence of reals is a sequence of fundamental sequences, so no choice is required. There seems to be an open question in regard to this, advertised by Alex Simpson and Martin Escardo: find a topos in which Cauchy reals are not Cauchy complete (i.e., not every Cauchy sequence of reals has a limit). For extra credit, make it so that the Cauchy completion of Cauchy reals is strictly smaller than the Dedekind reals. Has this been advertised on this list already? Or was it the FOM list? [If anyone replies to this, I suggest you start a new discussion thread.] Andrej Bauer From rrosebru@mta.ca Wed Jan 22 13:56:02 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 22 Jan 2003 13:56:02 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18bP24-0006uH-00 for categories-list@mta.ca; Wed, 22 Jan 2003 13:51:24 -0400 From: Martin Escardo MIME-Version: 1.0 Message-ID: <15918.28389.594290.761117@acws-0054.cs.bham.ac.uk> Date: Wed, 22 Jan 2003 10:13:57 +0000 To: CATEGORIES LIST Subject: categories: Cauchy completeness of Cauchy reals In-Reply-To: References: X-Mailer: VM 6.89 under 21.1 (patch 14) "Cuyahoga Valley" XEmacs Lucid Content-Type: text/plain; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 36 Andrej Bauer writes: > find a topos in which Cauchy reals > are not Cauchy complete (i.e., not every Cauchy sequence of reals has > a limit). For extra credit, make it so that the Cauchy completion of > Cauchy reals is strictly smaller than the Dedekind reals. One small clarification: Regarding the extra credit, there doesn't seem to be a reasonable "absolute" way of defining the completion in question. E.g. the various, constructively different, notions of metric completion already assume the existence of some given complete reals. However, one can always embed the Cauchy reals into the Dedekind reals, which are always Cauchy complete, and then look at the smallest "subset" containing this which is closed under limits of Cauchy sequences (where Cauchy sequences are defined as in Andrej's message). We sometimes call this, somewhat verbosely, "the Cauchy completion of the Cauchy reals within the Dedekind reals". But notice that this is the same as what one gets starting from the rationals within the Dedekind reals and then closing under limits and hence could be called the "Cauchy completion of the rationals within the Dedekind reals". NB. Freyd characterized the Dedekind reals as a final coalgebra. Alex Simpson and I characterized "the Cauchy completion of the rationals within the Dedekind reals" as a free algebra (to be precise, we started from the algebras as a primitive notion and later found this construction of the free one). But this has already been discussed in postings in the past few years. Martin Escardo From rrosebru@mta.ca Thu Jan 23 13:27:04 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 23 Jan 2003 13:27:04 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18bl4L-0004C9-00 for categories-list@mta.ca; Thu, 23 Jan 2003 13:23:13 -0400 Message-ID: <000b01c2c2c4$eba605e0$b1e493d9@alg1> From: "Mamuka Jibladze" To: References: <15918.28389.594290.761117@acws-0054.cs.bham.ac.uk> Subject: categories: Re: Cauchy completeness of Cauchy reals Date: Thu, 23 Jan 2003 13:50:00 +0400 MIME-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 7bit X-Priority: 3 X-MSMail-Priority: Normal X-Mailer: Microsoft Outlook Express 5.50.4807.1700 X-MimeOLE: Produced By Microsoft MimeOLE V5.50.4807.1700 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 37 > NB. Freyd characterized the Dedekind reals as a final coalgebra. Alex > Simpson and I characterized "the Cauchy completion of the rationals > within the Dedekind reals" as a free algebra (to be precise, we > started from the algebras as a primitive notion and later found this > construction of the free one). But this has already been discussed in > postings in the past few years. > > Martin Escardo Does one get any known versions of reals by performing the Cauchy or Dedekind construction starting with initial algebras I for non-decidable lifts L instead of the NNO? It would be then also natural to interpret Cauchy sequences and completeness using appropriate I-indexed families, of course. Even for "integers" Z one has at least three different options: taking I^op+1+I, taking the colimit of I->LI->LLI->..., each map being the unit, or taking the colimit of the corresponding I-indexed diagram. It would be strange if these turn out to be isomorphic. Is any of them an initial algebra for some simple functor? Similarly there are various possibilities for rationals - taking fractions, i.e. a quotient of ZxZ, or colimit of all multiplication maps Z->Z, or of the corresponding Z-indexed diagram. Actually I have not followed the ongoing research for a while, so maybe my questions are outdated. I would be grateful for any references to related work. Mamuka Jibladze From rrosebru@mta.ca Thu Jan 23 13:27:04 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 23 Jan 2003 13:27:04 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18bl2K-00044A-00 for categories-list@mta.ca; Thu, 23 Jan 2003 13:21:08 -0400 Date: Wed, 22 Jan 2003 15:33:00 -0800 From: Dusko Pavlovic User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.0.1) Gecko/20021003 X-Accept-Language: en-us, en MIME-Version: 1.0 To: CATEGORIES LIST Subject: categories: Re: Cauchy completeness of Cauchy reals References: <15918.28389.594290.761117@acws-0054.cs.bham.ac.uk> Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 38 Martin Escardo wrote: >NB. Freyd characterized the Dedekind reals as a final coalgebra. Alex >Simpson and I characterized "the Cauchy completion of the rationals >within the Dedekind reals" as a free algebra > and vaughan pratt and i characterized the cauchy reals as a final coalgebra. the papers are i proceedings of CMCS 99 and in TCS 280. in fact, freyd came up with his characterization of the closed interval while commenting on our first paper, where vaughan and i worked with the semiopen interval. but it is fair to say that the algebraic approach allows easier algebraic operations on reals. (i only managed to multiply them in one of our coalgebras, and in a very inefficient way.) -- dusko BTW have you seen the book: Life Itself. A Comprehensive Inquiry Into the Nature, Origin, and Fabrication of Life by Robert Rosen (Columbia University Press 1991) it was referenced in a biology paper, i found it in the biology library, and it's full of categories. (yes, i kno, people often do that to sound complicated, but this seems like honest work, perhaps even inspiring, although it does not go very deep.) From rrosebru@mta.ca Thu Jan 23 13:27:04 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 23 Jan 2003 13:27:04 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18bl5n-0004H2-00 for categories-list@mta.ca; Thu, 23 Jan 2003 13:24:43 -0400 Message-ID: <3E2FD9E8.3AB87032@sussex.ac.uk> Date: Thu, 23 Jan 2003 12:02:48 +0000 Organization: University of Sussex X-Mailer: Mozilla 4.72 [en] (Windows NT 5.0; U) X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Cauchy completions From: C.J.Mulvey@sussex.ac.uk (Christopher Mulvey) Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 39 The construction of the reals as the Cauchy completion of the rationals was worked out in full and glorious detail in the Montreal spring of 1973. The point is that taking equiconvergence classes of Cauchy sequences fails to construct the reals in a topos because of the absence generally of countable choice. Take your favourite example of a topos in which this fails, and you are most of the way to having your counter-example. To obtain the constructive version of the Cauchy reals, coinciding with the Dedekind reals in any topos with natural number object, you need to think a little more carefully about you are trying to achieve. The important thing about a Dedekind real is that there exist rationals that are arbitrarily close to it. The problem is that of choosing an instance of a rational at distance < 1/n from the real for each n. If you have countable choice, then choose away, get a Cauchy sequence, and have an isomorphism of Cauchy reals with Dedekind reals. Without countable choice, you still have an inhabited subset of the rationals consisting of all rationals at a distance of < 1/n from the Dedekind cut. This gives you a sequence of such subsets - a Cauchy approximation to the real. The constructive version of the Cauchy reals is the set of equiconvergence classes of Cauchy approximations on the rationals. For the details, later extended to the context of seminormed spaces over the rationals, with the set of rationals as the canonical example, see papers such as Burden/Mulvey in SLN 753 and my paper Banach sheaves in JPAA 17, 69-83 (1980). In the present context, the question is whether you wish to study the deficiencies of toposes in which countable choice fails, in which case Cauchy sequences are for you, or whether you want to develop constructive analysis within a topos, in which case you need to look at Cauchy approximations instead. Ask yourself, when you take a point in the closure of a subset, do you get handed a Cauchy sequence converging to it, or a sequence of possible choices of elements within 1/n of it if only you had countable choice to choose them. If the former, go for Cauchy sequences and count your blessings. If the latter, work with Cauchy approximations, which are every bit as powerful as Cauchy sequences and with respect to which the reals are Cauchy complete. Of course, the approach to Banach spaces through completeness defined in terms of Cauchy approximations acquires collateral justification in terms of the approaches to Banach sheaves taken by Auspitz and Banaschewski, to which reference can be found in the papers above. It is also the approach that allows Gelfand duality to be established constructively between commutative C*-algebras and compact completely regular locales in work with Banaschewski and with Vermeulen. Chris Mulvey. From rrosebru@mta.ca Thu Jan 23 13:27:04 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 23 Jan 2003 13:27:04 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18bl32-00046g-00 for categories-list@mta.ca; Thu, 23 Jan 2003 13:21:52 -0400 X-Mailer: exmh version 2.1.1 10/15/1999 To: CATEGORIES LIST Subject: categories: Re: Cauchy completeness of Cauchy reals In-Reply-To: Message from Martin Escardo of "Wed, 22 Jan 2003 10:13:57 GMT." <15918.28389.594290.761117@acws-0054.cs.bham.ac.uk> Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Mime-Version: 1.0 Content-Transfer-Encoding: quoted-printable Date: Wed, 22 Jan 2003 22:29:51 -0800 From: Vaughan Pratt Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 40 Dear toposophers, With constructivity of real arithmetic back on the front burner for the moment, let P be the ring of bounded power series a0 + a1.x + a2.x^2 + ..= =2E with integer coefficients a_i, where the bound is, for each such series, an integer c such that |a_i| < c (3/2)^i / i^(3/2). Let 1-2x generate the ideal I of P. Then the quotient ring P/I turns out= to be the field of reals [AMM 105(1998), p.769]. This is more constructive than it might appear, being just an obscure (or clear depending on your upbringing) way of representing reals in a redundant binary notation. The ring P permits fast arithmetic essentiall= y by deferring carries. Carries are "propagated" when needed by quotientin= g by I, which works by collapsing every formal power series to one all of whose coefficients other than a0 are either 0 or 1 and which has infinite= ly many 0s (equivalently, no infinite run of 1's). In this view of things, a real is understoood as an integer (a0) plus a binary fraction in [0,1) (the rest of some "binary" formal power series, meaning one with a_i =3D 0 or 1 for i > 0 and infinitely many 0s). A gen= eral formal power series without this restriction to 0 and 1 then constitutes a redundant representation of a real, which can be made irredundant when needed (e.g. when comparing with <) by quotienting by I. An intuitively clear but less constructive view is to evaluate each serie= s at x =3D 1/2, the root of 1-2x, noting that any series bounded as above conv= erges absolutely there. Series identified by I are those that evaluate to the same real at x =3D 1/2. What is nonconstructive about this is that direct evaluation of an infini= te series at a point requires infinite time, no matter how large and paralle= l the infinite circuit computing it may be. In contrast, P and P/I are more constructive in the following sense. Addition and subtraction in P require circuit depth O(1) using an infinit= e circuit whose gates perform integer addition and subtraction (just do it coordinatewise). Reduction mod I takes longer, but there is a variant of= the above in which it is fast enough. Instead of the field R we settle for just the group R, and instead of |a_i| < c (3/2)^i / i^(3/2) we settl= e for simply |a_i| < c. In this case any given series can be reduced (same= generator 1-2x) to the above normal form in circuit depth log_2(c) (nice exercise), a finite quantity despite the series itself being of infinite length and fluctuating arbitrarily within =B1c. Multiplication is problematic for two reasons. First it obliges the weak= er bound, complicating reduction. Secondly it is a convolution, complicatin= g arithmetic even when carry propagation is deferred. I don't see obvious solutions to either of these problems. On the other hand I have no a pri= ori reason to suppose that these circuit-theoretic complications of passing from R as a group to R as a ring or field would be reflected in suitably constructive topos-theoretic developments of these notions. Vaughan Pratt From rrosebru@mta.ca Fri Jan 24 13:46:04 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 24 Jan 2003 13:46:04 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18c7lZ-0003X1-00 for categories-list@mta.ca; Fri, 24 Jan 2003 13:37:21 -0400 Message-ID: <3E3048D1.9FB9BBCE@csc.liv.ac.uk> Date: Thu, 23 Jan 2003 19:56:01 +0000 From: Peter McBurney X-Mailer: Mozilla 4.79 [en] (X11; U; Linux 2.4.18-10 i686) X-Accept-Language: en MIME-Version: 1.0 To: CATEGORIES LIST Subject: categories: Category Theory in Biology References: <15918.28389.594290.761117@acws-0054.cs.bham.ac.uk> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 41 Dusko -- > > BTW have you seen the book: > > Life Itself. A Comprehensive Inquiry Into the Nature, Origin, and > Fabrication of Life > by Robert Rosen (Columbia University Press 1991) > > it was referenced in a biology paper, i found it in the biology library, > and it's full of categories. (yes, i kno, people often do that to sound > complicated, but this seems like honest work, perhaps even inspiring, > although it does not go very deep.) An earlier book of Rosen's applying category theory to biology (or rather, speaking more carefully, exploring how one might conceive of applying category theory to biological domains) was: "Anticipatory Systems: Philosophical, Mathematical and Methodological Foundations" (Pergamon Press, Oxford, UK 1985) You may also be interested in this work by Andree Ehresmann and Jean-Paul Venbremeersch on a category-theoretic account of evolving systems, such as those found in biological domains: http://perso.wanadoo.fr/vbm-ehr/ Peter McBurney Department of Computer Science University of Liverpool From rrosebru@mta.ca Fri Jan 24 13:46:04 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 24 Jan 2003 13:46:04 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18c7kh-0003TM-00 for categories-list@mta.ca; Fri, 24 Jan 2003 13:36:27 -0400 Message-ID: <20030123193855.60042.qmail@web12201.mail.yahoo.com> Date: Thu, 23 Jan 2003 11:38:55 -0800 (PST) From: Galchin Vasili Subject: categories: (pre-)Sheaves To: categories@mta.ca MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 42 Hello, I am trying to get my mind around (pre-)sheaves. I have studied point set topology in the past, but I didn't run into the notion of local homeomorphism. It seems to me that every local homeomorphism is a homeomorphism (because in a topological space (X, T), X is always a neighorhood of any point in X). Am I correct? Regards, Bill Halchin From rrosebru@mta.ca Fri Jan 24 13:46:04 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 24 Jan 2003 13:46:04 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18c7qA-0003qH-00 for categories-list@mta.ca; Fri, 24 Jan 2003 13:42:06 -0400 Mime-Version: 1.0 X-Sender: street@hera.ics.mq.edu.au Message-Id: In-Reply-To: <15918.28389.594290.761117@acws-0054.cs.bham.ac.uk> Date: Fri, 24 Jan 2003 12:34:55 +1100 To: categories@mta.ca From: Ross Street Subject: categories: Re: Cauchy completeness of Cauchy reals Content-Type: text/plain; charset="us-ascii" ; format="flowed" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 43 With all this talk about real numbers, perhaps readers would be interested in my little paper (reporting an idea of Steve Schanuel): An efficient construction of the real numbers, Gazette Australian Math. Soc. 12 (1985) 57-58. which may be hard to find. However, a recent report of an undergraduate vacation project can be obtained at http://www.maths.mq.edu.au/~street/efficient.pdf This project convinced me that this construction is a good one for teaching undergraduates. Others have had this idea too. In particular, the following was recently posted on the math arXiv: Norbert A'Campo, A natural construction of the real numbers, arXiv:math.GN/0301015 v1 3 Jan 2003. With regards, Ross From rrosebru@mta.ca Fri Jan 24 13:46:23 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 24 Jan 2003 13:46:23 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18c7tJ-00043y-00 for categories-list@mta.ca; Fri, 24 Jan 2003 13:45:21 -0400 From: Alex Simpson X-Authentication-Warning: topper.inf.ed.ac.uk: apache set sender to als@localhost using -f To: categories@mta.ca Subject: categories: Re: Cauchy completions Message-ID: <1043375117.3e30a40d45dc3@mail.inf.ed.ac.uk> Date: Fri, 24 Jan 2003 02:25:17 +0000 (GMT) References: <3E2FD9E8.3AB87032@sussex.ac.uk> In-Reply-To: <3E2FD9E8.3AB87032@sussex.ac.uk> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit User-Agent: IMP/PHP IMAP webmail program 2.2.8 X-Originating-IP: 130.54.16.90 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 44 This is a reply to Chris Mulvey's and Mamuka Jibladze's messages. Chris Mulvey's message nicely illustrates Martin Escardo's point that there are different senses in which one might understand Cauchy completion. As Chris confirms, it has long been known that, in toposes not satisfying number-number choice, the Cauchy reals, i.e. the set of Cauchy sequences (with modulus) quotiented by the obvious equivalence, are problematic. Chris takes Cauchy complete to mean complete w.r.t. "Cauchy approximations" which he defines as: > Without countable choice, you still have an inhabited subset of the > rationals consisting of all rationals at a distance of < 1/n from the > Dedekind cut. This gives you a sequence of such subsets - a Cauchy > approximation to the real. As he remarks, it is well known that the Cauchy reals need not be Cauchy complete w.r.t. Cauchy approximations. Moreover, their "Cauchy completion" is the object of Dedekind reals. Thus, any of the familiar toposes in which Cauchy and Dedekind reals differ (e.g. sheaves on R) provides an example in which the Cauchy reals are not Cauchy complete w.r.t. Cauchy approximations. The above story repeats itself exactly if one changes the meaning of Cauchy completeness to mean completeness w.r.t. a suitable notion of "Cauchy" filter. However, Andrej Bauer was referring to Cauchy completeness in a different sense. A very natural definition of Cauchy completeness is to merely require completeness w.r.t. Cauchy sequences (with modulus) of elements. This is weaker than the definitions above. The open(?) question Andrej referred to is to find an example of a topos (if one exists) in which the Cauchy reals are not themselves Cauchy complete w.r.t. convergent sequences. For this, one of course requires a topos in which the Cauchy and Dedekind reals differ (as the latter are complete). However, the standard examples of such toposes (e.g. sheaves on R) do not answer the question, for, in them, the Cauchy reals do turn out to be complete w.r.t. sequences. One might object to the above question on the grounds that completeness w.r.t. sequences is not the "correct" notion in a topos. There is some validity to this. However, the question originally arose because Martin Escardo and I came up with a definition of an "interval object" (an object of a category corresponding to the closed interval [0,1] in much the same way that a "natural numbers object" corresponds to the natural numbers) that makes sense in the very general setting of an arbitrary category with finite products. When interpreted in Set, the interval object is the interval [0,1]. When interpreted in Top it is the interval with Euclidean topology. When interpreted in an elementary topos, the interval object turns out to be the interval [0,1] constructed within the "Cauchy completion w.r.t convergent sequences of the Cauchy reals within the Dedekind reals", where the quotes are, once again, because the phrase needs careful interpretation. For mathematical details, see our paper in LICS 2001 "A Universal Characterization of the Closed Euclidean Interval". Our approach apparently has something to say related to Mamuka Jiblaze's question. For us the interval is defined as an algebra (implementing an algebraic notion of convexity) freely generated by the object 1+1. In Top, one can replace 1+1 by Sierpinski space as the generating object, in which case the interval with the topology of lower semicontinuity (equivalently the Scott topology) is obtained. Similarly, in a topos, one might take non-decidable objects (e.g. interesting "dominances" in the sense of Rosolini) as generating objects. We have not pursued this latter direction at all, but it might be interesting to do so. Alex Simpson Alex Simpson, LFCS, Division of Informatics, Univ. of Edinburgh Email: Alex.Simpson@ed.ac.uk Tel: +44 (0)131 650 5113 Web: http://www.dcs.ed.ac.uk/home/als Fax: +44 (0)131 667 7209 From rrosebru@mta.ca Fri Jan 24 13:47:09 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 24 Jan 2003 13:47:09 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18c7u7-00047g-00 for categories-list@mta.ca; Fri, 24 Jan 2003 13:46:11 -0400 From: Martin Escardo MIME-Version: 1.0 Message-ID: <15920.65167.864071.575967@acws-0054.cs.bham.ac.uk> Date: Fri, 24 Jan 2003 08:51:27 +0000 To: CATEGORIES LIST Subject: categories: Re: Cauchy completeness of Cauchy reals In-Reply-To: X-Mailer: VM 6.89 under 21.1 (patch 14) "Cuyahoga Valley" XEmacs Lucid Content-Type: text/plain; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 45 Dusko Pavlovic writes: > >NB. Freyd characterized the Dedekind reals as a final coalgebra. Alex > >Simpson and I characterized "the Cauchy completion of the rationals > >within the Dedekind reals" as a free algebra > > > and vaughan pratt and i characterized the cauchy reals as a final > coalgebra. the papers are i proceedings of CMCS 99 and in TCS 280. I forgot to mention this --- I apologize. In your paper, you work in Set. Do you think your construction works in any topos? If so, what would "Cauchy reals" mean precisely in this general context? Thanks. ME From rrosebru@mta.ca Fri Jan 24 14:00:54 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 24 Jan 2003 14:00:54 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18c87R-0005Kt-00 for categories-list@mta.ca; Fri, 24 Jan 2003 13:59:57 -0400 Message-ID: <3E31703D.9030801@kestrel.edu> Date: Fri, 24 Jan 2003 08:56:29 -0800 From: Dusko Pavlovic User-Agent: Mozilla/5.0 (X11; U; Linux ppc; en-US; rv:0.9.9) Gecko/20020604 X-Accept-Language: en-us, en MIME-Version: 1.0 To: CATEGORIES LIST Subject: categories: Re: Cauchy completeness of Cauchy reals References: Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 46 Andrej Bauer wrote: >There seems to be an open question in regard to this, advertised by >Alex Simpson and Martin Escardo: find a topos in which Cauchy reals >are not Cauchy complete (i.e., not every Cauchy sequence of reals has >a limit). For extra credit, make it so that the Cauchy completion of >Cauchy reals is strictly smaller than the Dedekind reals. > this will give me negative credits one way or another, but here it goes: let a = (a_i) be a cauchy sequence of rationals between 0 and 1. (cauchy means |a_m - a_n| < 1/m + 1/n, as in andrej's message.) let b = (b_i) be the subsequence b_i = a_{2^i+3}. b and a are equivalent in the sense from the message, because |a_m - b_n| < 1/m + 1/(2^n+3) < 2/m + 2/n note that |b_i - b_{i+k}| < 1/(2^i+3) + 1/(2^(i+k)+3) < 1/(2^i+2) now define x_i to be the simplest dyadic that falls in the interval between b_i - 1/2^(i+2) and b_i + 1/2^(i+2). in other words, to get x_i, begin adding 1/2 + 1/4 + 1/8... until you overshoot b_i - 1/2^(1+2). if you also overshoot b_i + 1/2^(1+2), and the last summand was 1/2^k, skip it, and try adding 1/2^(k+1), etc. one of them must fall in between. a less childish way to say this is that x_i is the shortest irredundant binary (no infinite sequences of 1) such that |b_i - x_i| < 1/2^(i+2) so x = (x_i) is a cauchy sequence equivalent to b, with |x_i - x_{i+k}| <= |x_i-b_i| + | b_i - b_{i+k}| + |b_{i+k} - x_{i+k}| < < 1/2^(i+2) + 1/2^(i+2) + 1/2^(i+k+2) < < 1/2^i this means that the first i digits of x_i and x_{i+k} coincide. now let X be the binary number such that its first i digits are the same as in x_i, for every i. (if it ends on an infinte sequence of 1s, replace it by the corresponding irredundant representative.) this is clearly a constant cauchy sequence equivalent to x, so it is its limit. since x is equivalent to b |b_m - x_n| <= |b_m - b_n| + |b_n - x_n| < 1/2^(m+3) + 1/2^(n+3) + 1/2^(n+2) < 2/m + 2/n and b is equivalent to a, X is also the limit of a. is there an error in the above reasoning? i can't find it. on the other hand, i printed out the paper by alex and martin, and the conjecture is stated rather strongly, so i guess i must be missing something. -- dusko From rrosebru@mta.ca Fri Jan 24 14:30:45 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 24 Jan 2003 14:30:45 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18c8Zy-0007bc-00 for categories-list@mta.ca; Fri, 24 Jan 2003 14:29:26 -0400 X-Sender: vitale@mail.math.ucl.ac.be Message-Id: Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" X-Mailer: Eudora Light F3.1.3l Date: Fri, 24 Jan 2003 20:23:36 +0100 To: categories@mta.ca From: Enrico Vitale Subject: categories: TAC Special Volume Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 47 TAC Special Volume, Call For Papers Dear Colleagues, Among the many important events which occurred in 2002 was the 60th birthday of Aurelio Carboni. With the approval of the Editorial Board of Theory and Applications of Categories, we wish to honour our friend and colleague Aurelio with a special issue of TAC. Following the editorial policy of TAC, we welcome papers that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. Authors are invited to submit their manuscripts in electronic form to any of the Guest Editors no later than September 15, 2003; articles will appear as soon as they are accepted. Authors are asked to prepare their manuscripts following the author information described at http://www.tac.mta.ca/tac/authinfo.html All papers will be carefully refereed following the standards of Theory and Applications of Categories. Guest Editors: George Janelidze george_janelidze@hotmail.com Steve Lack stevel@maths.usyd.edu.au Bill Lawvere wlawvere@buffalo.edu Enrico Vitale vitale@math.ucl.ac.be Richard Wood rjwood@mathstat.dal.ca From rrosebru@mta.ca Sat Jan 25 10:50:09 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 25 Jan 2003 10:50:09 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18cR7l-0001cp-00 for categories-list@mta.ca; Sat, 25 Jan 2003 10:17:33 -0400 Message-Id: <200301241249.h0OCnGF09312@mendieta.science.uva.nl> Date: Fri, 24 Jan 2003 13:49:16 +0100 X-Organisation: Faculty of Science, University of Amsterdam, The Netherlands X-URL: http://www.science.uva.nl/ From: info@folli.org To: categories@mta.ca Subject: categories: [ESSLLI03] 1st Call Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 48 ESSLLI 2003 15th European Summer School in Logic, Language and Information August 18-29, Vienna http://www.logic.at/esslli03/ Each year the European Association for Logic, Language and Information, (FoLLi) organizes a European Summer School (ESSLLI) the main focus of which is the interface between linguistics, logic and computation. Courses at foundational, introductory and advanced level are given, the aim of which is to provide for researchers and postgraduate as well as advanced master students the possibility to familiarize themselves with other areas of research, and to enable students and researchers to acquire more specialized knowledge about topics they are already familiar with. The school also features several workshops, and a student session in which Master and PhD students can present their work. This year the 15th ESSLLI Summer School will take place at the Technical University of Vienna, the beautiful and cultural capital of Austria. During two weeks 43 courses will be given. They cover a wide variety of topics within the combined areas of interest: Language and Logic, Language and Computation, and Logic and Computation. There will be a series of invited lectures, and several workshops with open calls for papers. Please, visit our website at http://www.logic.at/esslli03/ for detailed information. For information about FoLLi and the previous editions of ESSLLI see http://www.folli.org/ Deadline of the early registration: June 15, 2003. For other information please send an email to: esslli03@logic.at International Program Committee: Ivana Kruijff-Korbayova (chair) Alexander Leitsch (co-chair) Karen Sparck Jones Gosse Bouma Wojciech Buszkowski Johan Bos Thomas Eiter Ian Horrocks Local Organizing Committee Matthias Baaz (chair) Arnold Beckmann Agata Ciabattoni Rosalie Iemhoff Norbert Preining Sebastiaan Terwijn From rrosebru@mta.ca Sat Jan 25 10:50:10 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 25 Jan 2003 10:50:10 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18cR9h-0001hS-00 for categories-list@mta.ca; Sat, 25 Jan 2003 10:19:33 -0400 Date: Fri, 24 Jan 2003 11:49:25 -0800 (PST) From: "M. Healy" To: categories@mta.ca Subject: categories: Category theory and biological systems Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 49 Since the subject has been mentioned, I'd like to point to our investigation of the semantics of neural networks using category theory. It started much more recently than Andree's, of which I became aware only a year or two ago. We differ somewhat in approach, although we've been using some of Andree's ideas. My partner Tom Caudell and I have been doing research in neural networks for many years, our approach being a combination of mathematics and cognitive neuroscience. We started applying category theory in our semantic modeling a few years ago and are now developing architectures from it. Some references are easily accessible on my web page at http://cialab.ee.washington.edu . I'm under Affiliate Faculty, and there's a link to publications near the bottom of my home page. The categorical ones are conference papers, toward the bottom of the publications page (though if you're that interested, please let me send you a corrected version of the 2000 Como paper). We welcome feedback as well as questions. Mike =========================================================================== e Michael J. Healy A FA ----------> GA mjhealy@u.washington.edu | | | | 13544 23rd Place NE Ff | | Gf Seattle, WA 98125 | | USA \|/ \|/ ' ' FB ----------> GB e "I'm a natural man." B ============================================================================ From rrosebru@mta.ca Sat Jan 25 10:50:10 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 25 Jan 2003 10:50:10 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18cRBA-0001mJ-00 for categories-list@mta.ca; Sat, 25 Jan 2003 10:21:04 -0400 Message-ID: <3E31F48C.90308@kestrel.edu> Date: Fri, 24 Jan 2003 18:21:00 -0800 From: Dusko Pavlovic User-Agent: Mozilla/5.0 (X11; U; Linux ppc; en-US; rv:0.9.9) Gecko/20020604 X-Accept-Language: en-us, en MIME-Version: 1.0 To: CATEGORIES LIST Subject: categories: Re: Cauchy completeness of Cauchy reals References: <15920.65167.864071.575967@acws-0054.cs.bham.ac.uk> Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 50 > > >Set. Do you think your construction works in any topos? > the coalgebraic structures are defined using just arithmetic. in the first one, there is the "no infinite sequences of 1s" condition, which i am reminded depends on markov's principle; but that is just used in the explanation. i don't think there are other constraints. >If so, what >would "Cauchy reals" mean precisely in this general context? > it means fundamental sequence, with the equivalence relation in the "lazy" mode, a la bishop, as described in andrej bauer's message. if my last night's posting makes sense, then these constructivist cauchy reals make a whole lot of difference, because they really let you avoid the choice and get limits. -- dusko From rrosebru@mta.ca Sat Jan 25 10:50:10 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 25 Jan 2003 10:50:10 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18cR94-0001fi-00 for categories-list@mta.ca; Sat, 25 Jan 2003 10:18:54 -0400 Message-ID: <3E3198A9.9060902@kestrel.edu> Date: Fri, 24 Jan 2003 11:48:57 -0800 From: Dusko Pavlovic User-Agent: Mozilla/5.0 (X11; U; Linux ppc; en-US; rv:0.9.9) Gecko/20020604 X-Accept-Language: en-us, en MIME-Version: 1.0 To: CATEGORIES LIST Subject: categories: Re: Cauchy completeness of Cauchy reals References: <3E31703D.9030801@kestrel.edu> Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 51 heh, i typed this late, and managed to confuse the basic assumption. instead of > let a = (a_i) be a cauchy sequence of rationals between 0 and 1. let a = (a_i) be a cauchy sequence of *cauchy reals*, i.e. each a_i is a cauchy sequence of rationals between 0 and 1. i think the rest goes unchanged: you take a fast converging subsequence b of a, and then approximate b by irredundant rational prefixes. the irredundant representation is thus used instead of choice. the completeness of such representation is the finality of its coalgebraic structure. -- dusko From rrosebru@mta.ca Sat Jan 25 16:54:14 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 25 Jan 2003 16:54:14 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18cWzW-0000Ov-00 for categories-list@mta.ca; Sat, 25 Jan 2003 16:33:26 -0400 Message-ID: <3E323767.4060006@kurims.kyoto-u.ac.jp> Date: Sat, 25 Jan 2003 16:06:15 +0900 From: Alex Simpson User-Agent: Mozilla/5.0 (X11; U; SunOS sun4u; en-US; rv:1.1) Gecko/20020829 X-Accept-Language: en-us, en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Re: Cauchy completeness Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 52 Dusko Pavlovic writes: > is there an error in the above reasoning? i can't find it. on the > other > hand, i printed out the paper by alex and martin, and the conjecture > is > stated rather strongly, so i guess i must be missing something. Yes there is an error; but, more importantly, you are not answering the original question. Regarding the error, your argument is as follows. You start off with a Cauchy sequence a = (a_i) of rationals between 0 and 1. Using this you claim to find a binary expansion X such that X = lim a. Your construction of X is by: > now let X be the binary number such that its first i digits are the > same > as in x_i, for every i. (if it ends on an infinte sequence of 1s, > replace it by the corresponding irredundant representative.) This is not a valid intuitionistic definition, because the property of ending in an infinite sequence of 1s is not (logically) decidable. In fact,the internal statement that every Cauchy real in [0,1] has a binary expansion fails in many toposes (e.g. it fails in the effective topos). As is well known, this can be easily patched by, e.g., allowing 1/2 as an extra digit in binary expansions. Then one does obtain that every Cauchy real (in [0,1]) has such an "extended" binary expansion. However, none of this addresses the original question: > There seems to be an open question in regard to this, advertised by > Alex Simpson and Martin Escardo: find a topos in which Cauchy reals > are not Cauchy complete (i.e., not every Cauchy sequence of reals has > a limit). For this question, one must first construct the Cauchy reals R_C, e.g. as Cauchy sequences quotiented by equivalence, or, equivalently, as extended binary representations quotiented by equivalence. The question is: does every Cauchy sequence (x_i) in R_C have a limit in R_C? Here we are not starting off with a Cauchy sequence of rationals; not even a Cauchy sequence of Cauchy sequences. Instead (x_i) is a Cauchy sequence of equivalence classes of Cauchy sequences. To construct a limit, one apparently needs some choice to select representatives from each x_i. Thus it appears that the Cauchy completeness of R_C should fail in general. We would like to have an example of a topos in which it does fail. (Of course if there exists one such example then it also fails in the free topos with nno, but this is no help.) Alex Simpson Alex Simpson, RIMS, Kyoto University, Kyoto, Japan Permanent address: LFCS, Division of Informatics, Univ. of Edinburgh Email: Alex.Simpson@ed.ac.uk Web: http://www.dcs.ed.ac.uk/home/als From rrosebru@mta.ca Sat Jan 25 16:54:15 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 25 Jan 2003 16:54:15 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18cX0i-0000T9-00 for categories-list@mta.ca; Sat, 25 Jan 2003 16:34:40 -0400 Date: Sat, 25 Jan 2003 16:24:37 +0000 (GMT) From: "Prof. Peter Johnstone" To: CATEGORIES LIST Subject: categories: Re: Cauchy completeness of Cauchy reals In-Reply-To: <3E31F48C.90308@kestrel.edu> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Scanner: exiscan for exim4 (http://duncanthrax.net/exiscan/) *18cT6k-0003uj-00*vPtaD.U54TA* Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 53 On Fri, 24 Jan 2003, Dusko Pavlovic wrote: > > > > > >Set. Do you think your construction works in any topos? > > > the coalgebraic structures are defined using just arithmetic. in the > first one, there is the "no infinite sequences of 1s" condition, which i > am reminded depends on markov's principle; but that is just used in the > explanation. i don't think there are other constraints. > > >If so, what > >would "Cauchy reals" mean precisely in this general context? > > > it means fundamental sequence, with the equivalence relation in the > "lazy" mode, a la bishop, as described in andrej bauer's message. > I'm sorry, but this won't do. In a topos, equality is equality; you can't treat it "lazily". So a Cauchy real has to be an equivalence class of Cauchy sequences, and there is in general no way of choosing a canonical representative for it. Markov's principle would, I think (I haven't checked the details), suffice to give a canonical representation as a binary expansion with no infinite sequence of 1's, and then Dusko's argument would suffice to show that the Cauchy reals are Cauchy complete. But there are many toposes where Markov's principle fails. I doubt very much whether the Cauchy reals occur as a final coalgebra for anything, in any topos where they fail to coincide with the Dedekind reals, simply because the Dedekind reals are likely to be a coalgebra for the same endofunctor (and they're more "final" than the Cauchy reals). Incidentally, Peter Freyd and I worked out how to do his coalgebra construction constructively, and I showed that its final coalgebra is the Dedekind interval in any topos -- the proof is in the Elephant, at the end of section D4.7. Peter Johnstone From rrosebru@mta.ca Sat Jan 25 16:54:15 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 25 Jan 2003 16:54:15 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18cX23-0000WL-00 for categories-list@mta.ca; Sat, 25 Jan 2003 16:36:03 -0400 Message-Id: <3.0.5.32.20030125175944.0085c8c0@mailhost.cs.bham.ac.uk> X-Sender: sjv@mailhost.cs.bham.ac.uk X-Mailer: QUALCOMM Windows Eudora Light Version 3.0.5 (32) Date: Sat, 25 Jan 2003 17:59:44 +0000 To: categories@mta.ca From: S Vickers Subject: categories: Re: (pre-)Sheaves In-Reply-To: <20030123193855.60042.qmail@web12201.mail.yahoo.com> Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 54 At 11:38 23/01/03 -0800, Bill Halchin wrote: > I am trying to get my mind around (pre-)sheaves. I have studied point >set topology in the past, but I didn't run into the notion of local >homeomorphism. It seems to me that every local homeomorphism is a >homeomorphism (because in a topological space (X, T), X is always a >neighorhood of any point in X). Am I correct? Dear Bill, Absolutely not. Consider the definition of local homeomorphism for a map f: X -> 1. If f is a local homeomorphism then every x in X has an open neighbourhood homeomorphic to 1, and you find in fact that f is a local homeomorphism iff X has the discrete topology. One way to think of a local homeomorphism f: X -> Y is that the stalk map stalk(y) = f^{-1}({y}) is a "continuous map from Y to the class of sets". Of course, the class of sets is not a topological space. (This isn't just a problem of size - there really is no suitable topology.) Hence "continuity" here is a new concept and that is what the definition of local homeomorphism captures. But intuitively it makes some sense. The definition ensures that if y jiggles about infinitesimally then the set stalk(y) makes no sudden jumps - no new elements suddenly come into existence, nor any equalities between elements. I hope you can see something of this intuition; if not, don't worry but just stick to the definition. The definition ensures that each stalk, as a subspace of X, has discrete topology, so it really is a set, not a more general space. All the non-discrete topology in X arises across the stalks, as homeomorphic copies of bits of topology on Y. Topology within the stalks is discrete. Topos theory is able to make some formal sense of the intuition. There is a topos E whose class of points (not objects) is the class of sets. It is called the "object classifier". If I (naughtily, you might think) write Y for the topos of sheaves over Y, then geometric morphisms from Y to E are just sheaves over Y. But it is legitimate to think of geometric morphisms between toposes as continuous maps between their points - this certainly works for toposes of sheaves over spaces, at least if the spaces are nice enough (sober). Then geometric morphisms from Y to E should be thought of a continuous maps from Y to the class of sets, as I said before. Steve Vickers. From rrosebru@mta.ca Sun Jan 26 09:58:02 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 26 Jan 2003 09:58:02 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18cnA9-0002sQ-00 for categories-list@mta.ca; Sun, 26 Jan 2003 09:49:29 -0400 Message-Id: <200301252120.NAA26529@coraki.Stanford.EDU> X-Mailer: exmh version 2.1.1 10/15/1999 To: categories@mta.ca Subject: categories: What does it take to identify the field and the continuum of reals? Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Mime-Version: 1.0 Content-Transfer-Encoding: quoted-printable Date: Sat, 25 Jan 2003 13:20:57 -0800 From: Vaughan Pratt Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 55 By way of motivating the question posed in the subject line I'll pick up in the middle of this thread on Dedekind vs. Cauchy reals, which I can't help much with I'm afraid but which provides a nice jumping off point for= my real topic nonetheless. >From: Martin Escardo > >From: Dusko Pavlovic > > >From: Martin Escardo > > >NB. Freyd characterized the Dedekind reals as a final coalgebra. Ale= x > > >Simpson and I characterized "the Cauchy completion of the rationals > > >within the Dedekind reals" as a free algebra > > > > > and vaughan pratt and i characterized the cauchy reals as a final > > coalgebra. the papers are i proceedings of CMCS 99 and in TCS 280. > >I forgot to mention this --- I apologize. In your paper, you work in >Set. Do you think your construction works in any topos? If so, what >would "Cauchy reals" mean precisely in this general context? Thanks. I would bounce this question back to Martin: what did he mean by "the Dedekind reals" in his attribution to Freyd? Both the Pavlovic-Pratt and Freyd constructions of the continuum as a fin= al coalgebra characterize the continuum only up to its order type (and hence= up to homeomorphism if we take the usual order topology generated by the open intervals). Cuts in the *field* Q of rationals inherit Q's metric, but cuts in the *poset* Q acquire only topology. Only with Q qua poset would it be fair to say that either Peter's or our coalgebraic construction of the continuum "characterized the Dedekind rea= ls." The Cauchy completion of the rationals on the other hand requires Q to be= at minimum a metric space and surely a field if you want to bring in 1/n.= This distinction constitutes a disconnect between Martin's first two sentences that subsequent emails are at risk of propagating. I have not to date seen any really convincing marriage of the algebraic and coalgebraic approaches to defining real numbers. The very fact that algebra produces the field of reals while coalgebra produces the continuu= m as understood by descriptive set theorists draws a sharp line right there= between the two approaches. The only marriage I'm aware of that even works at all is Conway's elegant= construction of his surreal numbers. It is a marriage because (loosely speaking) the numbers entering on the ends create algebra while those interpolating their predecessors in the Conway ordering create coalgebra.= A great virtue of this construction is its complete lack of any distincti= on between, or even reference to, algebra and coalgebra, the implicit presen= ce of both notwithstanding. Unfortunately it produces neither the field of reals nor a continuum. Conway doesn't get the former because just before day omega he has only produced the ring of binary fractions, those rationals of the form m/2^n.= Day omega itself however witnesses the birth not only of all the remainin= g reals but the first few infinities and infinitesimals, in particular =B1w and their reciprocals. This doesn't even form an additive monoid le= t alone a ring since w+w for example is not due to arrive for another w day= s! Negation is the only arithmetic operation surviving the day-to-day evolut= ion of Conway's surreal universe, from its little bang to its apocalyptic Fie= ld. Seeking closure, Conway slogs gamely on through *all* the ordinals to pro= duce a Field of reals. (Or rather The Field, the maximal such having been sho= wn elsewhere to be unique, if I've understood that correctly.) This being a= proper class, not only does it not have the cardinality of the continuum,= it doesn't have a cardinality at all! Now I conjecture that stopping just before day \epsilon_0, for the sake o= f getting a set, produces a field closed under all functions whose n-th bit= is computable in time f(n) where f is definable in Peano arithmetic. And it= may well be that Conway already has a field just before day \omega^\omega= , I haven't checked but surely someone has by now (I'm very bad at keeping up with these things, sorry). But all this is for naught here, since even the smallest Conway field wha= tever it might turn out to be is cannot be Archimedean, for the reason above. And although it has the power of the continuum it lacks its order type: with the usual order topology, the Conway continuum becomes totally disconnected as soon as =B11 appear, and remains that way thenceforth. Total disconnectedness is not anything a continuum can be proud of. It seems to me that topos theory, or logic, or something in between if that makes sense, should have something to say about a gap between the algebra and coalgebra of the reals. Algebraically the reals form a field= , coalgebraically they form a continuum. What is the logical strength of the weakest framework identifying these dual views of the reals? Vaughan Pratt From rrosebru@mta.ca Mon Jan 27 12:33:44 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 27 Jan 2003 12:33:44 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18dC91-0000pw-00 for categories-list@mta.ca; Mon, 27 Jan 2003 12:29:59 -0400 From: Martin Escardo MIME-Version: 1.0 Message-ID: <15925.7427.766854.416003@acws-0054.cs.bham.ac.uk> Date: Mon, 27 Jan 2003 11:50:27 +0000 To: categories@mta.ca Subject: categories: Re: What does it take to identify the field and the continuum of reals? In-Reply-To: <200301252120.NAA26529@coraki.Stanford.EDU> References: <200301252120.NAA26529@coraki.Stanford.EDU> X-Mailer: VM 6.89 under 21.1 (patch 14) "Cuyahoga Valley" XEmacs Lucid Content-Type: text/plain; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 56 Vaughan Pratt writes: > I would bounce this question back to Martin: what did he mean by "th= e > Dedekind reals" in his attribution to Freyd? I meant (and still mean): the underlying object of the final coalgebra is what topos theorists know as "the object of Dedekind reals" (in an elementary topos with nno). In more detail [Freyd & Johnstone, in Johnstone's Elephant, pages 1028-1032]: given a topos with nno, consider the category of (internal) posets in the topos. In this category, define a functor. Consider its final coalgebra. Theorem: (1) It exists. (2) Moreover, the underlying object of the algebra is the Dedekind unit interval under its natural order. (3) The structure map performs average (x,y) |-> (x+y)/2 (for full details, see the reference). Answering the question quoted below, you get all the ingredients you are looking for: a *set* of numbers (as the underlying set of the underlying poset of the final coalgebra), its *order* (as the underlying object of the final coalgebra), and (part of) its *algebraic* structure (as the structure map of the final coalgebra). Of course, here "set" means an object of a topos, e.g. that of classical sets. You get only part of the *algebraic* structure, but topos logic is strong enough to allow you to fully recov= er=20 it after you have the final coalgebra in your hands.=20 The Escardo-Simpson approach is similar, but takes a different route and makes weaker assumptions - I won't repeat the story, which can be found in the paper whose reference was already given by Alex Simpson. Martin Escardo From rrosebru@mta.ca Mon Jan 27 12:33:44 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 27 Jan 2003 12:33:44 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18dC5t-0000ZI-00 for categories-list@mta.ca; Mon, 27 Jan 2003 12:26:45 -0400 Date: Sun, 26 Jan 2003 15:25:37 -0800 From: Toby Bartels To: categories@mta.ca Subject: categories: Re: What does it take to identify the field and the continuum of reals? Message-ID: <20030126232537.GB9502@math-lw-n06.ucr.edu> References: <200301252120.NAA26529@coraki.Stanford.EDU> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <200301252120.NAA26529@coraki.Stanford.EDU> User-Agent: Mutt/1.4i Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 57 Vaughan Pratt wrote in part: [about Conway's surreal numbers] >Now I conjecture that stopping just before day \epsilon_0, for the sake of >getting a set, produces a field closed under all functions whose n-th bit is >computable in time f(n) where f is definable in Peano arithmetic. And it >may well be that Conway already has a field just before day \omega^\omega, >I haven't checked but surely someone has by now (I'm very bad at keeping >up with these things, sorry). It's my understanding that you don't get a field until (just before) day K for K an inaccessible cardinal number. I'm not 100% certain about this, however! -- Toby Bartels From rrosebru@mta.ca Mon Jan 27 12:33:44 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 27 Jan 2003 12:33:44 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18dC75-0000g0-00 for categories-list@mta.ca; Mon, 27 Jan 2003 12:27:59 -0400 From: Alex Simpson X-Authentication-Warning: topper.inf.ed.ac.uk: apache set sender to als@localhost using -f To: categories@mta.ca Subject: categories: Re: Cauchy completeness of Cauchy reals Message-ID: <1043639865.3e34ae39d965f@mail.inf.ed.ac.uk> Date: Mon, 27 Jan 2003 03:57:45 +0000 (GMT) References: In-Reply-To: MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit User-Agent: IMP/PHP IMAP webmail program 2.2.8 X-Originating-IP: 130.54.16.90 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 58 Peter Johnstone writes: > I'm sorry, but this won't do. In a topos, equality is equality; you > can't > treat it "lazily". So a Cauchy real has to be an equivalence class of > Cauchy sequences, and there is in general no way of choosing a > canonical representative for it. Markov's principle would, I think > (I haven't checked the details), suffice to give a canonical > representation as a binary expansion with no infinite sequence of > 1's, In fact not. Markov's principle holds in the effective topos, and there, unless I'm much mistaken, it is not even true that the map from binary representations to Cauchy (= Dedekind) reals in [0,1] is epi, let alone split epi. Alex Simpson Alex Simpson, LFCS, Division of Informatics, Univ. of Edinburgh Email: Alex.Simpson@ed.ac.uk Tel: +44 (0)131 650 5113 Web: http://www.dcs.ed.ac.uk/home/als Fax: +44 (0)131 667 7209 From rrosebru@mta.ca Mon Jan 27 19:41:59 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 27 Jan 2003 19:41:59 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18dIpk-0003BF-00 for categories-list@mta.ca; Mon, 27 Jan 2003 19:38:32 -0400 To: categories@mta.ca Subject: categories: Re: Cauchy completeness of Cauchy reals Reply-To: Andrej Bauer From: Andrej Bauer Date: 27 Jan 2003 18:41:39 +0100 In-Reply-To: Alex Simpson's message of "Mon, 27 Jan 2003 03:57:45 +0000 (GMT)" Message-ID: User-Agent: Gnus/5.0807 (Gnus v5.8.7) XEmacs/21.4 (Common Lisp) MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 59 Alex Simpson writes: > In fact not. Markov's principle holds in the effective topos, and > there, unless I'm much mistaken, it is not even true that the map from > binary representations to Cauchy (= Dedekind) reals in [0,1] is epi, > let alone split epi. The map e : 2^N --> [0,1] defined by e x = x_0/2 + x_1/4 + x_2/8 + ... is epi in the effective topos, but it is not regular epi. In terms of logic, this means that forall a : [0,1]. (not not (exists x : 2^n. (e x = a))) is valid in the effective topos, but forall a : [0,1]. (exists x : 2^n. (e x = a)) is not valid. Andrej From rrosebru@mta.ca Tue Jan 28 19:56:07 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 28 Jan 2003 19:56:07 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18dfUt-0003BT-00 for categories-list@mta.ca; Tue, 28 Jan 2003 19:50:31 -0400 From: Alex Simpson X-Authentication-Warning: topper.inf.ed.ac.uk: apache set sender to als@localhost using -f To: categories@mta.ca Subject: categories: Two questions on the real numbers Message-ID: <1043731719.3e3615076aca9@mail.inf.ed.ac.uk> Date: Tue, 28 Jan 2003 05:28:39 +0000 (GMT) MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit User-Agent: IMP/PHP IMAP webmail program 2.2.8 X-Originating-IP: 130.54.16.90 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 60 While the topic is still hot, I'd like to post two more questions concerning the various real number objects. Just to recap, in any elementary topos with nno N we have the Cauchy reals R_C, the Dedekind reals R_D, and also the "Cauchy-completion (w.r.t. sequences) of R_C in R_D", as discussed thoroughly in previous postings. Let's call this latter object R_E. All three objects are logically defined, and hence preserved by logical functors between toposes. Martin Escardo and I proved that R_E is also preserved by inverse image functors of essential geometric morphisms. (Actually, we proved this for the closed unit interval I_E in R_E. The result for R_E follows by exibiting R_E as a coequalizer of two well-chosen maps from N x I_E to itself.) QUESTION 1. What preservation results are available for R_C and R_D? Surely something is known about this. I can't, at the moment, see any reason for them to be preserved by inverse image functors of arbitrary essential geometric morphisms. Interesting mathematical differences between the objects arise when one considers algebraic closure properties of the complex numbers C_C, C_D and C_E associated with R_C, R_D and R_E respectively. In Fourman and Hyland, "Sheaf models for analysis" (Springer LNM 753, 1979) it is shown that the Dedekind complex numbers C_D are not in general algebraically closed. This fails in the strong sense that, in certain toposes, one can actually exhibit a polynomial that has no root. Thus the fundamental theorem of algebra does not hold in general for C_D. On the other hand, in Ruitenberg, "Constructing roots of polynomials over the complex numbers" (in "Computational aspects of Lie group representations and related topics", CWI Tract 84, Amsterdam, 1990), it is shown that the fundamental theorem of algebra does hold for C_C in any topos. (I first heard about this paper from Fred Richman. I have never seen it. I have only read its math review, no.92g:03085.) The conflicting picture above, leads naturally to: QUESTION 2. Does the fundamental theorem of algebra hold for C_E? I would be interested to hear any ideas at all related to these questions. Alex Simpson Alex Simpson, LFCS, Division of Informatics, Univ. of Edinburgh Email: Alex.Simpson@ed.ac.uk Tel: +44 (0)131 650 5113 Web: http://www.dcs.ed.ac.uk/home/als Fax: +44 (0)131 667 7209 From rrosebru@mta.ca Tue Jan 28 19:56:07 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 28 Jan 2003 19:56:07 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18dfXn-0003N4-00 for categories-list@mta.ca; Tue, 28 Jan 2003 19:53:31 -0400 Message-ID: <3E36ED4F.4070807@kestrel> Date: Tue, 28 Jan 2003 12:51:27 -0800 From: Dusko Pavlovic User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.0.1) Gecko/20021003 X-Accept-Language: en-us, en MIME-Version: 1.0 To: CATEGORIES mailing list Subject: categories: Re: Cauchy completeness of Cauchy reals Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 61 [this is a copy of my post of monday morning, which bounced between bob and me a couple of times, courtesy of our mailers. -- dusko] thanks for the replies. sorry to clog people's mailboxes, but i'll permit myself one more post on cauchy. (i think this does deserve some general interest because we often say that categories capture real mathematical practices --- but as it happens, cauchy reals are not complete, and the mean value theorem fails, and so on. i was hoping to understand where does the usual intuition of continuum fail, and what categorical property do we need to do basic calculus. i came to think that coalgebras help with this, since they capture the various notions of completeness, and wondered why they don't capture the standard cauchy completeness argument in this context. hence my post that invoked the reactions.) On Sat, 25 Jan 2003 Prof. Peter Johnstone wrote: >>>> > >If so, what >>>> > >would "Cauchy reals" mean precisely in this general context? >>>> > > >>> >>> >>> > it means fundamental sequence, with the equivalence relation in the >>> > "lazy" mode, a la bishop, as described in andrej bauer's message. >>> > >> >> >> I'm sorry, but this won't do. In a topos, equality is equality; you can't >> treat it "lazily". So a Cauchy real has to be an equivalence class of >> Cauchy sequences, and there is in general no way of choosing a >> canonical representative for it. > > one would hope that equality in a topos is widely understood, even by me. treating fundamental sequences up to an equivalence relation in a lazy mode just means not taking their quotient, but carrying the explicit equivalence relation. such structures are commonly considered in toposes. on the other hand, many constructivists (martin-lof, bishop) say that this is the way to do constructivist mathematics. (although i am not sure whether i came to think of cauchy reals in this way because constructivist education left some trace, or because undergraduate analysis didn't.) sorry i didn't make all this clear. martin escardo's remark to which i responded was rather cursory, he just attributed two things, so i kept mine short. moreover, toposes were not mentioned, and as far as i remember, the validity in toposes was not discussed either by freyd, or by vaughan and me. we all talked about streams of digits and it seemed to me that we were talking about cauchy reals (the constructivist ones), until peter johnstone observed that freyd = dedekind++. On Sat, 25 Jan 2003 Alex Simpson wrote: >> The question is: does every Cauchy sequence (x_i) in R_C have a >> limit in R_C >> >> Here we are not starting off with a Cauchy sequence of rationals; >> not even a Cauchy sequence of Cauchy sequences. > > i realized that i typed "let a = (a_i) be a sequence of rationals" instead of "a sequence of cauchy reals" as soon as i woke up, the morning after i typed it, and sent a correction a couple of hours after the post --- but our watchful moderator for some reason didn't forward it to the list. in any case, i said i thought that the construction went through for cauchy sequences of constructivist cauchy reals, as described in andrej bauer's message: >> (2) we say that a real _is_ a fundamental sequence, where two reals >> are claimed "equal" if they coincide (the approach taken by Bishop). > > now it turns out that such cauchy reals don't count, that cauchy reals must be >> (1) we say that a real is an equivalence class of fundamental >> sequences under the relation ~, > > well, call me irresponsible, but i think that the same idea still applies: the irredundant coalgebraic reals give canonical representatives for equivalence classes too. with them, one can prove completeness as usually. here is a slight modification of sequences from my previous post. let Q be the set of rationals between 0 and 1, D <= Q dyadic rationals and N natural numbers. a cauchy real A is now a subobject of Q^N such that exists x in A forall x in A holds: |xm - xn| < 1/m+1/n forall x in A and all y in Q^N holds: |xm - yn| < 2/m+2/n iff y in A. consider maps b: Q^N --> Q^N, c: Q^N --> D^N and d : D^N --> Q^N, defined b(x)i = x(2^(i+3)) c(x)i = p/2^n, such that |xi - p/2^n| < 1/2^(i+2) and |xi - q/2^m| < 1/2^(i+2) implies m>=n of q>=p d(x)i = x truncated after i'th digit ** i claim that the image dcb(A) of A along is a representative of A, ie ** ** 1. it is a singleton, and ** 2. an element of A. this means that the function dcb : Q^N-->Q^N induces a choice function from Q^N/~ to Q^N, assigning to each cauchy real a cauchy sequence of ratioanls representing it. the proofs proceed like for the corresponding sequences in my previous post. in particular, for every x,y : A holds |cb(x)i - cb(y)i| <= |cb(x)i - b(x)i| + |b(x)i-b(y)i| + |b(y)i-cb(y)i| < < 1/2^(i+2) + 2/2^(i+3)+2/2^(i+3) + 1/2^(i+2) = = 1/2^i means that cb(x)i and cb(y)i have the first i digits equal. hence dcb(x)i =dcb(y)i. since this holds for all i, dcb(x) = dcb(y). now, as everyone has been pointing out, the dyadic representation depends on markov's principle. in order to prove that the map c is total, we need the fact that for every e>0 in Q there is some k such that 1/2 + 1/4 +...+ 1/2^k > 1-e. in other words, that there is k s.t. 1/2^k < e. this is *equivalent* to markov's principle. how bad is markov's principle? well, i think that markov proposed it as a valid *intuitionistic* principle: ** given an algorithm, if i can prove that it terminates, then i ** should be able to construct its output. it would be nice to know that this is all we need in order to have cauchy complete cauchy reals. also, if this is the case, the challenge topos, where cauchy reals are not complete, would be the realizability topos invalidating markov: the cauchy sequence without a cauchy limit would have to be the one that can be proven different from 0, but cannot be proven apart from 0. is there still an error? please ignore the trivial ones this time, and i'll try to learn from errors. all the best, -- dusko From rrosebru@mta.ca Tue Jan 28 19:56:07 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 28 Jan 2003 19:56:07 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18dfWW-0003HU-00 for categories-list@mta.ca; Tue, 28 Jan 2003 19:52:12 -0400 To: categories@mta.ca Subject: categories: Re: Cauchy completeness of Cauchy reals Reply-To: Andrej Bauer From: Andrej Bauer Date: 28 Jan 2003 10:44:41 +0100 In-Reply-To: Alex Simpson's message of "Tue, 28 Jan 2003 01:50:18 +0000 (GMT)" Message-ID: User-Agent: Gnus/5.0807 (Gnus v5.8.7) XEmacs/21.4 (Common Lisp) MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 62 Alex Simpson writes: > > > The map e : 2^N --> [0,1] defined by > > > > e x = x_0/2 + x_1/4 + x_2/8 + ... > > > > is epi in the effective topos, but it is not regular epi. > > This is clearly wrong. Every epi is regular, in a topos. > > My original statement was correct. In the effective topos, > the map from binary representations to Cauchy (= Dedekind) > reals is not epi. I stand corrected. I am confusing the effective topos with assemblies (or modest sets) over the first Kleene algebra. Andrej From rrosebru@mta.ca Tue Jan 28 19:56:07 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 28 Jan 2003 19:56:07 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18dfTu-00037Z-00 for categories-list@mta.ca; Tue, 28 Jan 2003 19:49:30 -0400 From: Alex Simpson X-Authentication-Warning: topper.inf.ed.ac.uk: apache set sender to als@localhost using -f To: categories@mta.ca Subject: categories: Re: Cauchy completeness of Cauchy reals Message-ID: <1043718618.3e35e1da24c25@mail.inf.ed.ac.uk> Date: Tue, 28 Jan 2003 01:50:18 +0000 (GMT) In-Reply-To: MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit User-Agent: IMP/PHP IMAP webmail program 2.2.8 X-Originating-IP: 130.54.16.90 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 63 Andrej Bauer writes: > The map e : 2^N --> [0,1] defined by > > e x = x_0/2 + x_1/4 + x_2/8 + ... > > is epi in the effective topos, but it is not regular epi. This is clearly wrong. Every epi is regular, in a topos. My original statement was correct. In the effective topos, the map from binary representations to Cauchy (= Dedekind) reals is not epi. Alex Simpson Alex Simpson, LFCS, Division of Informatics, Univ. of Edinburgh Email: Alex.Simpson@ed.ac.uk Tel: +44 (0)131 650 5113 Web: http://www.dcs.ed.ac.uk/home/als Fax: +44 (0)131 667 7209 From rrosebru@mta.ca Wed Jan 29 11:40:48 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 29 Jan 2003 11:40:48 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18duJ2-0005C2-00 for categories-list@mta.ca; Wed, 29 Jan 2003 11:39:16 -0400 From: Alex Simpson To: CATEGORIES mailing list Subject: categories: Re: Cauchy completeness of Cauchy reals Message-ID: <1043829334.3e37925619e77@mail.inf.ed.ac.uk> Date: Wed, 29 Jan 2003 08:35:34 +0000 (GMT) References: <3E36ED4F.4070807@kestrel> In-Reply-To: <3E36ED4F.4070807@kestrel> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit User-Agent: IMP/PHP IMAP webmail program 2.2.8 X-Originating-IP: 130.54.16.90 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 64 Dear Dusko, > is there still an error? please ignore the trivial ones this time, and > i'll try to learn from errors. Yes, I think there's an error. > here is a slight modification of sequences from my previous post. let > Q be the set of rationals between 0 and 1, D <= Q dyadic rationals and > N natural numbers. a cauchy real A is now a subobject of Q^N such that > > [... construction omitted ...] > > the proofs proceed like for the corresponding sequences in my previous > post. in particular, for every x,y : A holds > > |cb(x)i - cb(y)i| <= [... calculation omitted ...] > <= 1/2^i > > means that cb(x)i and cb(y)i have the first i digits equal. hence > dcb(x)i =dcb(y)i. since this holds for all i, dcb(x) = dcb(y). I don't see that cb(x)i and cb(y)i have the first i digits equal. It seems possible to have e.g. cb(x)i = .0111 and cb(y)i = .1000. Indeed, .0111, although it is sufficiently close to b(x)i to be the value of cb(x)i, may nonetheless be too far from b(y)i to qualify as a "simpler" candidate for cb(y)i than .1000. This problem is not easily repaired. In fact, there is a fundamental obstacle to this approach. Your argument attempts to construct a function f: Q^N --> Q^N (in your proof given by f=dcb) satisfying: 1. f maps any Cauchy sequence to a Cauchy sequence representing the same real number. 2. All sequences that represent the same real number get mapped to a single unique Cauchy sequence representative. Such an f is tantamount to giving a splitting to the epi r: {x: Q^N | x a Cauchy sequence} --> I_C where I_C is the Cauchy interval. There are many toposes in which Q^N is basically Baire space and I_C is basically the closed unit interval in Euclidean space (e.g. Johnstone's "topological topos", many "Gros toposes"). In such toposes, a splitting of r would correspond to a non-constant continuous function from the Euclidean interval to Baire space. This is clearly impossible, as Baire space is totally disconnected. Furthermore, in many such toposes (e.g. Johnstone's), countable choice and Markov's principle both hold. In conclusion, it is impossible to prove the existence of an f satisfying 1 and 2 above using intuitionistic logic, even if one further assumes countable choice and Markov's principle. Regarding Markov's principle: > now, as everyone has been pointing out, the dyadic representation > depends on markov's principle. This is *not* what has been pointed out (whatever you mean by dyadic representation). It is well-known that, in general, very many different versions of Cauchy sequence coincide, including: Cauchy sequences of rationals, indeed many variants depending on properties of the modulus; ditto for sequences of dyadic rationals; nested sequences of closeed proper intervals; "signed" binary representation, etc, etc. What I previously pointed out was that the existence of ordinary binary representations may fail even in the presence of Markov's principle. > in order to prove that the map c is > total, we need the fact that for every e>0 in Q there is some k such > that 1/2 + 1/4 +...+ 1/2^k > 1-e. in other words, that there is k > s.t. 1/2^k < e. this is *equivalent* to markov's principle. The property quoted is in fact a trivial consequence of intuitionistic arithmetic alone. It has nothing to do with Markov's principle. Indeed your function c is total in any elementary topos. > how bad is markov's principle? well, i think that markov proposed it > as a valid *intuitionistic* principle: > > ** given an algorithm, if i can prove that it terminates, then i > ** should be able to construct its output. This is a curious paraphrasing. It should rather be: "if the algorithm cannot fail to terminate then ..." > it would be nice to know that this is all we need in order to have > cauchy complete cauchy reals. It would be nice and may be true. At present we don't have a single example topos in which the Cauchy reals are not complete (w.r.t. sequences). However, there is, as yet, no convincing reason to link Markov's principle to this question. Best wishes, Alex Alex Simpson, LFCS, Division of Informatics, Univ. of Edinburgh Email: Alex.Simpson@ed.ac.uk Tel: +44 (0)131 650 5113 Web: http://www.dcs.ed.ac.uk/home/als Fax: +44 (0)131 667 7209 From rrosebru@mta.ca Wed Jan 29 11:40:48 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 29 Jan 2003 11:40:48 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18duHt-00057O-00 for categories-list@mta.ca; Wed, 29 Jan 2003 11:38:06 -0400 Date: Tue, 28 Jan 2003 18:00:12 -0800 From: Toby Bartels To: CATEGORIES mailing list Subject: categories: Re: Cauchy completeness of Cauchy reals Message-ID: <20030129020011.GA29763@math-lw-n01.ucr.edu> References: <3E36ED4F.4070807@kestrel> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <3E36ED4F.4070807@kestrel> User-Agent: Mutt/1.4i Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 65 Dusko Pavlovic wrote in part: >(i think this does deserve some general interest because we often say >that categories capture real mathematical practices --- but as it >happens, cauchy reals are not complete, and the mean value theorem >fails, and so on. i was hoping to understand where does the usual >intuition of continuum fail, and what categorical property do we need >to do basic calculus. It depends on what you mean by "basic calculus". Bishop would argue that he can do basic calculus just fine using a constructive version of the mean value theorem. This is not to say that you don't have an interesting question; from the POV of the mathematician on the street (not very theoretical), classical theorems often follow from constructivist (a la Bishop) one if you assume that sequentially compact metric spaces are compact (which means complete and totally bounded to Brouwer and Bishop), so that might be one place to look. -- Toby From rrosebru@mta.ca Thu Jan 30 14:55:09 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 30 Jan 2003 14:55:09 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18eJkw-0005IC-00 for categories-list@mta.ca; Thu, 30 Jan 2003 14:49:46 -0400 From: Igor Walukiewicz MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <15929.3531.44933.145006@gargle.gargle.HOWL> Date: Thu, 30 Jan 2003 12:34:35 +0100 To: categories@mta.ca Subject: categories: CFP: FICS 03 X-Mailer: VM 7.07 under 21.4 (patch 8) "Honest Recruiter" XEmacs Lucid Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 66 Fixed Points in Computer Science FICS'03 A Satellite Workshop to ETAPS'2003 12-13 April, 2003, Warsaw, Poland CALL FOR PAPERS Aim. Fixed points play a fundamental role in several areas of computer science and logic by justifying induction and recursive definitions. The construction and properties of fixed points have been investigated in many different frameworks such as: design and implementation of programming languages, program logics, databases. The aim of the workshop is to provide a forum for researchers to present their results to those members of the computer science and logic communities who study or apply the theory of fixed points. Previous workshops where held in Brno (1998, MFCS workshop), Paris (2000, LC2000 workshop), Florence (2001, PLI workshop). Copenhagen (2002, LICS workshop). Topics include, but are not restricted to: Construction and reasoning about properties of fixed points, categorical, metric and ordered fixed point models, continuous algebras, relation algebras, regular algebras of finitary and infinitary languages, formal power series, word and tree automata, the mu-calculus and other programming logics, fixed points in process algebras and process calculi, fixed points and the lambda calculus, fixed points in relation to dataflow and circuits, fixed points in logic programming, databases and complexity theory. Programme Committee: J. Adamek (Braunschweig) R. Amadio (Marseille) R. Backhouse (Nottingham) S. Bloom (Hoboken NJ) J. Bradfield (Edinburgh) A. Dawar (Cambridge) R. De Nicola (Florence) Z. Esik (cochair, Szeged) I. Guessarian (Paris) M. Mislove (Tulane) I. Walukiewicz (cochair, Bordeaux) Invited speakers: Martin Grohe (Edinburgh) Erich Gradel (Aachen) Damian Niwinski (Warsaw) Leszek Pacholski (Wroclaw) Contact person: Igor Walukiewicz LaBRI Domaine Universitaire, bat. A30 351, cours de la Liberation 33405 Talence Cedex FRANCE igw@labri.fr phone: +33 5 56.84.69.00 fax: +33 5 56.84.66.69 Paper submission: Authors are invited to send three copies of an abstract not exceeding three pages to Igor Walukiewicz. Electronic submissions in the form of uuencoded postscript files are encouraged and can be sent to igw@labri.fr. Submissions are to be received before February 14, 2003. Authors will be notified of acceptance by March 10, 2003. Proceedings: Preliminary proceedings containing the abstracts of the talks will be available at the meeting. Final proceedings will be published after the meeting as a special issue of Theoretical Informatics and Application (http://www.edpsciences.org/docinfos/ITA/). The meeting will be organized in affiliation to ETAPS'03: http://www.mimuw.edu.pl/etaps03 Important Dates: Submission: February 14, 2003 Notification: March 10, 2003 Final version of the abstract: March 17, 2003 More information is available at the web site http://www.labri.fr/~igw/fics From rrosebru@mta.ca Thu Jan 30 14:55:09 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 30 Jan 2003 14:55:09 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18eJj1-00058z-00 for categories-list@mta.ca; Thu, 30 Jan 2003 14:47:47 -0400 Mime-Version: 1.0 Message-Id: Date: Thu, 30 Jan 2003 14:33:35 +0100 To: categories@mta.ca From: Alessio Guglielmi Subject: categories: Proof Theory List Content-Type: text/plain; charset="us-ascii" ; format="flowed" X-Sender: 520008346700-0001@t-dialin.net Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 67 Hello, there is a new list dedicated to proof theory: please find more info and a list of subscribers at . -Alessio -- Alessio Guglielmi, PhD Department of Computer Science - Technische Universitaet Dresden Dresden - Germany From rrosebru@mta.ca Fri Jan 31 11:17:24 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 31 Jan 2003 11:17:24 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18ecsE-0007XC-00 for categories-list@mta.ca; Fri, 31 Jan 2003 11:14:34 -0400 Date: Thu, 30 Jan 2003 22:54:54 -0500 (EST) From: "P. Scott" To: categories@mta.ca Subject: categories: Fields Institute Summer School in Logic & Theoretical CS Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 68 Dear Colleagues: This is an update of the last announcement. June will be theoretical computer science month at U. Ottawa! The Field's Institute will sponsor a summer school in Logic and Foundations of Computation at the University of Ottawa this summer, June 2-20, 2003. This program will be hosted by the logic group in the Department of Mathematics and Statistics at the University of Ottawa (consisting of Philip Scott, Richard Blute, and Peter Selinger). The program will consist of 2 weeks of courses for graduate students, then a week of workshops in several areas of theoretical computer science. This program is particularly aimed at graduate students in mathematics, logic, theoretical computer science, mathematical linguistics and related areas. The program culminates in the 18th annual IEEE Logic in Computer Science (LICS2003) meeting at U. Ottawa June 21-27. For the latter, see http://www.dcs.ed.ac.uk/home/als/lics/. Weeks 1,2: Each week will consist of two courses (one in the morning, the other in the afternoon), taught by experts in the area. We are also expecting visiting experts, who may give informal seminars as well. We are planning topics that include: Week 1: (a) Categorical Logic and type theory and (b) Linear Logic. Lectures will be given by our logic group, as well as visiting scholars. Among the visitors we are pleased to have Thomas Ehrhard (Marseille), Robert Seely (McGill), and Robin Cockett (Calgary). Week 2: (a) Game Semantics and (b) Concurrency. We are honoured to announce that Samson Abramsky (Oxford) and Glynn Winskel (Cambridge), resp., will be lecturing on the two topics above. We hope to have other distinguished visitors who will give additional lectures. Week 3: Fields Institute Workshops. These include, among other topics, June 15-16: Quantum Programming Languages (Org: Peter Selinger), June 17: Game Semantics (In preparation) June 18-19: Mathematical Linguistics (Org: J. Lambek) June 19-20: Mobility Workshop (In preparation) Further details on these workshops will be forthcoming. Some limited funding scholarships will be made available to graduate students for attending the summer school. To apply for this money, we ask that you contact us and include the following information: 1) A one-page email letter stating your background as well as why you are interested in attending. 2) The letter should also state whether you have access to any other funding to attend. 3) An email letter of reference from your supervisor or an appropriate other person. Preference will be given to students working in the areas covered by the Fields Summer School. Applications should be received by February 28. Non-students are of course welcome to attend the summer school and/or workshops; there will be a nominal registration fee for attendance. For further information to apply, please contact any of us: Philip Scott (phil@site.uottawa.ca) Richard Blute (rblute@mathstat.uottawa.ca) Peter Selinger (selinger@mathstat.uottawa.ca) The Webpage of the Fields Institute Summer School in Logic and Theoretical Computer Science is: http://www.mathstat.uottawa.ca/lfc/fields2003/ From rrosebru@mta.ca Fri Jan 31 11:17:25 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 31 Jan 2003 11:17:25 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18ecuL-0007m5-00 for categories-list@mta.ca; Fri, 31 Jan 2003 11:16:45 -0400 Message-ID: <3E3A779E.8040008@inf.ed.ac.uk> Date: Fri, 31 Jan 2003 13:18:22 +0000 From: Gordon Plotkin Organization: Informatics User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.1) Gecko/20020930 X-Accept-Language: en-us, en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Chair of Theoretical Computer Science Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 69 Chair of Theoretical Computer Science, LFCS, School of Informatics, Edinburgh University The above chair is currently open; we seek outstanding candidates in any area of theoretical computer science. For details, see http://www.informatics.ed.ac.uk/events/vacancies/ Gordon Plotkin