*mbx* 42cf5a7e00000000 3-Dec-2002 18:58:24 -0400,968;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 03 Dec 2002 18:58:24 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18JLnu-0007ml-00 for categories-list@mta.ca; Tue, 03 Dec 2002 18:46:10 -0400 Message-ID: <20021202193708.80670.qmail@web12204.mail.yahoo.com> Date: Mon, 2 Dec 2002 11:37:08 -0800 (PST) From: Galchin Vasili Subject: categories: Topos construction question To: categories@mta.ca MIME-Version: 1.0 Sender: cat-dist@mta.ca Precedence: bulk Fact: In a topos, Hom (1, omega) is a Heyting algebra. Fact: A Heyting algebra is a CCC (closed catesian category). Question: is there a topos T where Hom (1, omega) itself is a topos or equivalently has a subobject classifier (in addition to being a CCC)? Question: If there is no such topos T, where can I find a proof that no such topos exists? Regards, Bill Halchin 4-Dec-2002 15:01:17 -0400,1265;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 04 Dec 2002 15:01:17 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18Jeea-0005pg-00 for categories-list@mta.ca; Wed, 04 Dec 2002 14:53:48 -0400 Message-ID: <20021204114148.37435.qmail@web14207.mail.yahoo.com> Date: Wed, 4 Dec 2002 03:41:48 -0800 (PST) From: Saeed Salehi Subject: categories: new position in Uppsala (Logic) To: categories@mta.ca MIME-Version: 1.0 Sender: cat-dist@mta.ca Precedence: bulk Dear Colleague, A position in mathematics directed towards mathematical logic at the assistant professor level (in analogy with the American system) has just been announced at Uppsala University, Sweden. The position is four 4 or 5 years, after which the position holder can apply for tenure. The position involves 60% research and 40% teaching. The applicant must have a Ph.D. and the degree must not be more than five years old. The deadline for application is 19 December 2002. For more information see: http://www.math.uu.se/inform/assistantprof_eng.php Please spread this information to anyone who may be interested in applying. Best wishes Viggo Stoltenberg-Hansen 4-Dec-2002 15:04:09 -0400,1951;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 04 Dec 2002 15:04:09 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18Jejb-0006BN-00 for categories-list@mta.ca; Wed, 04 Dec 2002 14:58:59 -0400 Date: Wed, 4 Dec 2002 11:46:18 +0000 (GMT) From: "Prof. Peter Johnstone" To: categories@mta.ca Subject: categories: Re: Topos construction question In-Reply-To: <20021202193708.80670.qmail@web12204.mail.yahoo.com> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Scanner: exiscan for exim4 (http://duncanthrax.net/exiscan/) *18JXyu-00072A-00*6kxBucn0E1k* Sender: cat-dist@mta.ca Precedence: bulk [note from moderator: before I had a chance to post this response, several other readers also pointed out the degeneracy involved, so those will not be posted. Regards, Bob] On Mon, 2 Dec 2002, Galchin Vasili wrote: > > Fact: In a topos, Hom (1, omega) is a Heyting algebra. > > Fact: A Heyting algebra is a CCC (closed catesian category). > > Question: is there a topos T where Hom (1, omega) itself is a topos or equivalently > > has a subobject classifier (in addition to being a CCC)? > > Question: If there is no such topos T, where can I find a proof that no such topos > > exists? > I'm not sure what Bill means by this question -- it seems to contain a category mistake (as the philosophers would say). Hom (1,\Omega) is always a partial order, but a topos can never be a partial order unless it is degenerate. Perhaps he is groping towards the notion of quasitopos, which is a common generalization of the notions of topos and of Heyting algebra -- see section A2.6 of "Sketches of an Elephant", or alternatively Oswald Wyler's book "Lecture Notes on Topoi and Quasitopoi". Peter Johnstone 6-Dec-2002 17:09:04 -0400,2949;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 06 Dec 2002 17:09:04 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18KPaS-00070g-00 for categories-list@mta.ca; Fri, 06 Dec 2002 17:00:40 -0400 To: categories@mta.ca Subject: categories: UWO/Fields homotopy theory program From: Dan Christensen Date: Fri, 06 Dec 2002 12:56:59 -0500 Message-ID: <87vg27hvys.fsf@uwo.ca> Lines: 67 MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Sender: cat-dist@mta.ca Precedence: bulk Second announcement Fields Institute Program on Applied Homotopy Theory University of Western Ontario London, Ontario September, 2003 http://www.math.uwo.ca/homotopy/ During the month of September, 2003, the Department of Mathematics at the University of Western Ontario will host a program on homotopy theory and its applications to other areas. Gunnar Carlsson, Paul Goerss, Ieke Moerdijk, Jack Morava and Fabien Morel will be in residence for some or all of the month. All of the events will take place in London, Ontario. The focus of the month will be a special 5 day version of the Ontario Topology Seminar, beginning on Saturday, September 20 in the morning and ending on Wednesday, September 24 in the afternoon. The speakers who have agreed to come are listed below. In addition, there will be several minicourses at other times during the month given by the five longer-term visitors. Each will consist of two to three lectures. The topics and dates will be announced later. We have received funding from the Fields Institute and additional funding is being sought from other agencies. We expect to be able to provide some support to graduate students and recent Ph.D.'s (contact us if you are eligible). The organizers are Rick Jardine and Dan Christensen . If you think you might attend, please let one of us know. The web page for this event is at http://www.math.uwo.ca/homotopy/ and will be updated periodically. Hotel and travel information is available at http://jdc.math.uwo.ca/directions.html We recommend you book a hotel room soon, as the conference overlaps with homecoming weekend at Western. (You can always cancel later.) Conference and mini-course speakers: Alejandro Adem, Wisconsin John Baez, Univ. of California, Riverside Paul Baum, Penn State Gunnar Carlsson, Stanford Wojciech Chacholski, Minnesota Bill Dwyer, Notre Dame Paul Goerss, Northwestern Jesper Grodal, Chicago Lars Hesselholt, MIT Mikhail Kapranov, Toronto Finnur Larusson, UWO Ib Madsen, Aarhus Peter May, Chicago Haynes Miller, MIT Ieke Moerdijk, Utrecht Jack Morava, Johns Hopkins Fabien Morel, Paris 7 Victor Snaith, Southampton Neil Strickland, Sheffield Bertrand Toen, Nice 6-Dec-2002 21:38:26 -0400,1216;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 06 Dec 2002 21:38:26 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18KTnI-0006mS-00 for categories-list@mta.ca; Fri, 06 Dec 2002 21:30:12 -0400 Date: Fri, 6 Dec 2002 15:10:41 +0000 (GMT) From: "Prof. Peter Johnstone" To: Categories mailing list Subject: categories: The Topos of Music Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Scanner: exiscan for exim4 (http://duncanthrax.net/exiscan/) *18KK7m-00020G-00*Ff1Zb3pRKGI* Sender: cat-dist@mta.ca Precedence: bulk While looking for something else, I came across a reference to a recent book called "The Topos of Music: Geometric Logic of Concepts, Theory and Performance" by G. Mazzola, published by Birkh"auser. Has anyone on the categories list seen this book? If so, can you say whether it is really about toposes and geometric logic as I (and most category-theorists) would understand those terms, or is it just a coincidence of terminology? Peter Johnstone 7-Dec-2002 10:09:32 -0400,1189;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 07 Dec 2002 10:09:32 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18KfRa-0005wL-00 for categories-list@mta.ca; Sat, 07 Dec 2002 09:56:34 -0400 Message-Id: <4.1.20021206165214.02ae10b0@mail.oberlin.net> X-Sender: cwells@mail.oberlin.net X-Mailer: QUALCOMM Windows Eudora Pro Version 4.1 Date: Fri, 06 Dec 2002 16:53:15 -0500 To: categories@mta.ca From: Charles Wells Subject: categories: Change of Address for Charles and Jane Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Sender: cat-dist@mta.ca Precedence: bulk We have new email addresses: cwells@oberlin.net (Charles) jwells@oberlin.net (Jane) The freude.com addresses will DISAPPEAR at the end of 2002! Charles and Jane Wells Charles Wells professional website: http://www.cwru.edu/artsci/math/wells/home.html personal website: http://www.oberlin.net/~cwells/index.html genealogical website: http://familytreemaker.genealogy.com/users/w/e/l/Charles-Wells/ NE Ohio Sacred Harp website: http://www.oberlin.net/~cwells/sh.htm 7-Dec-2002 10:09:32 -0400,1978;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 07 Dec 2002 10:09:32 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18KfTQ-00061g-00 for categories-list@mta.ca; Sat, 07 Dec 2002 09:58:28 -0400 X-Authentication-Warning: triples.math.mcgill.ca: barr owned process doing -bs Date: Fri, 6 Dec 2002 21:08:25 -0500 (EST) From: Michael Barr X-Sender: barr@triples.math.mcgill.ca To: Categories mailing list Subject: categories: Re: The Topos of Music In-Reply-To: Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Well, I don't know, but the book is by Mazzola et al and one of the als is named Stefan Muller who, according to Amazon.ca has a paper published in The arithmetic and geometry of algebraic cycles: Proceedings of the CRM summer school, June 7-19, 1998, Banff, Alberta, Canada (CRM is the Centre de Recherche Mathematiques.) He has other publications that seem similarly mathematical, although there would seem to be a fringe aspect to some of them. One of his books, published this year, is called Complex Predicates. The other authors do not have other publicatons listed on Amazon. On Fri, 6 Dec 2002, Prof. Peter Johnstone wrote: > While looking for something else, I came across a reference to a recent > book called "The Topos of Music: Geometric Logic of Concepts, Theory and > Performance" by G. Mazzola, published by Birkh"auser. Has anyone on the > categories list seen this book? If so, can you say whether it is really > about toposes and geometric logic as I (and most category-theorists) > would understand those terms, or is it just a coincidence of terminology? > > Peter Johnstone > > > > > 7-Dec-2002 10:09:32 -0400,1667;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 07 Dec 2002 10:09:32 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18KfUk-00066Q-00 for categories-list@mta.ca; Sat, 07 Dec 2002 09:59:50 -0400 From: "Robert L. Knighten" MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <15857.34864.795177.439588@zeus.knighten.org> Date: Fri, 6 Dec 2002 21:33:36 -0800 To: categories@mta.ca Subject: categories: Re: The Topos of Music In-Reply-To: References: X-Mailer: VM 7.04 under Emacs 21.2.1 Reply-To: Robert@Knighten.org (Robert L. Knighten) Sender: cat-dist@mta.ca Precedence: bulk Prof. Peter Johnstone writes: > While looking for something else, I came across a reference to a recent > book called "The Topos of Music: Geometric Logic of Concepts, Theory and > Performance" by G. Mazzola, published by Birkh"auser. Has anyone on the > categories list seen this book? If so, can you say whether it is really > about toposes and geometric logic as I (and most category-theorists) > would understand those terms, or is it just a coincidence of terminology? > > Peter Johnstone I've not yet seen the book, but I have looked at some of the related web sites. It is not "just a coincidence of terminology", though I don't understand if the usage of toposes, geometric logic, algebraic geometry, etc. is more than alegorical. -- Bob 7-Dec-2002 10:10:02 -0400,3687;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 07 Dec 2002 10:10:02 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18KfX3-0006CI-00 for categories-list@mta.ca; Sat, 07 Dec 2002 10:02:13 -0400 Date: Sat, 7 Dec 2002 06:34:03 -0500 (EST) From: Peter Freyd Message-Id: <200212071134.gB7BY3LW020283@saul.cis.upenn.edu> To: categories@mta.ca Subject: categories: Re: The Topos of Music Sender: cat-dist@mta.ca Precedence: bulk It just may, indeed, by our topoi and geometric logic: http://www.birkhauser.ch/books/math/5731.htm Mazzola, G., University of Zurich, Switzerland In Collaboration with Stefan Gvller and Stefan M|ller The Topos of Music Geometric Logic of Concepts, Theory, and Performance 2002. 1368 pages. Hardcover. incl. CD-ROM $ 98.- / CHF 144.- ISBN 3-7643-5731-2 Subscription price $ 98.- / CHF 144.- valid until 31.12.02 Regular Price: $ 128.- / CHF 188.- Since the Greek antiquity it has been a tradition of European thinking to describe musical facts in a mathematical language. This formal apparatus has always mirrored the status quo of mathematical knowledge and the requirements of current sound technology. The Topos of Music is the upgraded and vastly deepened English extension of the seminal German Geometrie der Tvne. It reflects the dramatic progress of mathematical music theory and its operationalization by information technology since the publication of Geometrie der Tvne in 1990. The conceptual basis has been vastly generalized to topos-theoretic foundations, including a corresponding thoroughly geometric musical logic. The theoretical models and results now include topologies for rhythm, melody, and harmony, as well as a classification theory of musical objects that comprises the topos-theoretic concept framework. Classification also implies techniques of algebraic moduli theory. The classical models of modulation and counterpoint have been extended to exotic scales and counterpoint interval dichotomies. The probably most exciting new field of research deals with musical performance and its implementation on advanced object-oriented software environments. This subject not only uses extensively the existing mathematical music theory, it also opens the language to differential equations and tools of differential geometry, such as Lie derivatives. Mathematical performance theory is the key to inverse performance theory, an advanced new research field which deals with the calculation of varieties of parameters which give rise to a determined performance. This field uses techniques of algebraic geometry and statistics, approaches which have already produced significant results in the understanding of highest-ranked human performances. The book's formal language and models are currently being used by leading researchers in Europe and Northern America and have become a foundation of music software design. This is also testified by the book's nineteen collaborators and the included CD-ROM containing software and music examples. Contributors: Carlos Agon, Moreno Andreatta, Girard Assayag, Jan Beran, Chantal Buteau, Roberto Ferretti, Anja Fleischer, Harald Fripertinger, Jvrg Garbers, Werner Hemmert, Michael Leyton, Emilio Lluis Puebla, Mariana Montiel Hernandez, Thomas Noll, Joachim Stange-Elbe, Hans Straub, Oliver Zahorka 7-Dec-2002 10:10:02 -0400,2307;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 07 Dec 2002 10:10:02 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18KfWM-0006AJ-00 for categories-list@mta.ca; Sat, 07 Dec 2002 10:01:30 -0400 Date: Sat, 7 Dec 2002 09:08:15 +0000 (GMT) From: Michael Abbott To: Categories mailing list Subject: categories: Re: The Topos of Music In-Reply-To: Message-ID: <20021207084715.L9888-100000@saturn.araneidae.co.uk> MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk On Fri, 6 Dec 2002, Prof. Peter Johnstone wrote: > While looking for something else, I came across a reference to a recent > book called "The Topos of Music: Geometric Logic of Concepts, Theory and > Performance" by G. Mazzola, published by Birkh"auser. Has anyone on the > categories list seen this book? If so, can you say whether it is really > about toposes and geometric logic as I (and most category-theorists) > would understand those terms, or is it just a coincidence of terminology? I have not seen the book, but a quick web search has been quite instructive[1,2,3,4,5]. The author is clearly writing about music theory, and deliberately using the language [2] and mathematics [3] of category and topos theory. The content of [3] seems to be more mathematics than music, but I doubt I can make much sense of either. It's hard for me to tell, but the evidence from the links below suggests that this is actually quite serious stuff, with an application of mathematics to the performance of music. References [1] Synopsis on amazon web site http://www.amazon.co.uk/exec/obidos/ASIN/3764357312/qid=1039250777/sr=1-1/ref=sr_1_0_1/026-0247167-1565262 [2] Mazzola, "Music Performance and Interpretation" http://www.engineeringandmusic.de/individu/mazzguer/maguproc.html [3] Mazzola, "Mathematical Music Theory -- Status Quo 2000" http://www.ircam.fr/equipes/repmus/mamux/documents/status.pdf [4] Homepage of "Engineering and Music" http://www.engineeringandmusic.de/ [5] Mazzola's own home page http://www.ifi.unizh.ch/staff/mazzola/ 7-Dec-2002 12:55:22 -0400,2845;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 07 Dec 2002 12:55:22 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18Ki9H-0000LB-00 for categories-list@mta.ca; Sat, 07 Dec 2002 12:49:51 -0400 Date: Sat, 7 Dec 2002 13:37:00 +0000 (GMT) From: "Prof. Peter Johnstone" To: Categories mailing list Subject: categories: Re: The Topos of Music In-Reply-To: Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Scanner: exiscan for exim4 (http://duncanthrax.net/exiscan/) *18Kf8e-0004y8-00*f5n02dl/2Gw* Sender: cat-dist@mta.ca Precedence: bulk On Fri, 6 Dec 2002, Prof. Peter Johnstone wrote: > While looking for something else, I came across a reference to a recent > book called "The Topos of Music: Geometric Logic of Concepts, Theory and > Performance" by G. Mazzola, published by Birkh"auser. Has anyone on the > categories list seen this book? If so, can you say whether it is really > about toposes and geometric logic as I (and most category-theorists) > would understand those terms, or is it just a coincidence of terminology? > > Peter Johnstone > To answer my own question, I have now managed to get hold of a copy of the book. It's a very large book (1360 pages, U.K. price 83.5 pounds) -- but I suppose it's not for me to complain about that. The author is indeed attempting to apply topos theory (and quite a lot of other high-powered mathematics) to the analysis of music. Whether there's any substance in it is hard to tell from a qick skim-through: I have a strong suspicion that the whole thing is skilfully crafted from bovine excrement, but I'll need to consult my colleagues in the Music Faculty to see whether they think there's anything in it. I am not cited in the Bibliography (naturally I checked this first!) but the books by Goldblatt and Mac Lane--Moerdijk are both there. Bill Lawvere is cited for ETCS (1964), but not for anything more recent. Alexander Grothendieck is cited for SGA4, and also for a private communication to the author, commenting on the book's German- language predecessor (published 1990): "Das ist wohl schon die Mathematik des 'Neuen Zeitalters'". Composers cited in the Bibliography are, in alphabetical order, Milton Babbitt, J.S. Bach, Pierre Boulez, Claude Debussy, J.J. Fux, Paul Hindemith, Sigfrid Karg-Elert, W.A. Mozart, Arnold Schoenberg, Franz Schubert, Robert Schumann and Anton Webern (I may have missed one or two). Other citations include Aristotle, Francis Bacon, Umberto Eco and (inevitably?) Douglas Hofstadter. Peter Johnstone 7-Dec-2002 13:09:29 -0400,1291;000000000000-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 07 Dec 2002 13:09:29 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18KiO6-0001Id-00 for categories-list@mta.ca; Sat, 07 Dec 2002 13:05:10 -0400 Message-Id: <200212071534.AAA27710@cc2002.kyoto-su.ac.jp> To: Categories mailing list Subject: categories: Re: The Topos of Music Mime-Version: 1.0 (generated by tm-edit 7.48) Content-Type: text/plain; charset=US-ASCII Date: Sun, 08 Dec 2002 00:34:50 +0900 From: Hiroyuki Miyoshi Sender: cat-dist@mta.ca Precedence: bulk I obtained that thick book of Mazzola et al a few days ago. They try to analyse and synthesize various aspects of music with mathematical structures. They construct such structures from the category of modules and borrow some techniques from algebraic geometry, but formal logic does not appear in it. They also utilize works in computer science for their purpose and indeed has developed their software for musical composition and performance. It might be interesting as an application of mathematical conceptions. I would like to suspend my judgement on the value of this book until using the software. Hiroyuki Miyoshi 9-Dec-2002 09:36:41 -0400,2221;000000000000-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 09 Dec 2002 09:36:41 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18LNwV-0006Ey-00 for categories-list@mta.ca; Mon, 09 Dec 2002 09:27:27 -0400 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 To: categories@mta.ca From: "Al Vilcius" Subject: categories: concatenation X-Sent-From: remote@vilcius.com Date: Sat, 07 Dec 2002 18:49:34 -0800 (PST) X-Mailer: Web Mail 5.1.1-3_sol28 Message-Id: <20021207184934.20088.h001.c015.wm@mail.vilcius.com.criticalpath.net> Sender: cat-dist@mta.ca Precedence: bulk concatenation of lists and streams from an alphabet A: - formally given by the unique arrow to a terminal coalgebra - heuristically it is supposed to be thought of as =93erasing the comma=94 = between a pair of streams (a,b) But how is this to be understood computationally? eg. write down all the +ve odd integers and then all the even ones in rever= se order to get a stream (1, 3, 5, =85=85=85., 6, 4, 2) can this be made into a stream specification?=20 ie. what is the behaviour of the =93dots=94 in the middle? or even more interesting, a countable concatenation (limit ?) as in the so called Sarkovskii sequence uses in symbolic dynamics - Ref: http://hades.ph.tn.tudelft.nl/Internal/PHServices/Documentation/MathWorld/m= ath/math/s/s035.htm It does not appear conceivable for a Turing machine to produce such a tape!= (??) Then in what way can such streams be seen as arrows N --> N ?? Examining the details (Ref: J.J.M.M. Rutten) for the construction of the structure map=20 A*xA* --> 1+AxA*xA* that gives rise to concatenation (for the functor 1+Ax_= ), it does not appear to arise out of universal properties=20 (being an arrow from a product to a coproduct),=20 as do the structure maps for various other operations. Is it distinguished in some particular way? I think of juxtaposition as THE fundamental syntactic operation =96 I hope someone can help me please with formal concatenation. Thank you. =85.. Al Vilcius 9-Dec-2002 09:36:41 -0400,978;000000000000-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 09 Dec 2002 09:36:41 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18LNyV-0006Nq-00 for categories-list@mta.ca; Mon, 09 Dec 2002 09:29:31 -0400 From: Topos8@aol.com Message-ID: <1a2.d132280.2b24ba49@aol.com> Date: Sun, 8 Dec 2002 10:07:53 EST Subject: categories: twisted morphism category To: categories@mta.ca MIME-Version: 1.0 Sender: cat-dist@mta.ca Precedence: bulk I've been reading Lawvere's 1970 paper "Equality in hyperdoctrines and comprehension schema...." which appeared in the AMS series Symposia in Pure Mathematics, volume 17, pp 1-14. In the first line on page 12 he refers to the " 'twisted morphism category' " B^ and the forgetful functor from B^ to (B op) x (B). Can someone explain what this twisted morphism category is and/or provide a reference to the definition? Thanks for your help. Carl Futia 9-Dec-2002 11:11:56 -0400,1875;000000000000-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 09 Dec 2002 11:11:56 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18LPVt-0005eS-00 for categories-list@mta.ca; Mon, 09 Dec 2002 11:08:05 -0400 From: Nikita Danilov MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <15860.44716.555516.899126@laputa.namesys.com> Date: Mon, 9 Dec 2002 17:54:36 +0300 X-PGP-Fingerprint: 43CE 9384 5A1D CD75 5087 A876 A1AA 84D0 CCAA AC92 X-PGP-Key-ID: CCAAAC92 X-PGP-Key-At: http://wwwkeys.pgp.net:11371/pks/lookup?op=get&search=0xCCAAAC92 To: categories@mta.ca Subject: categories: Re: twisted morphism category In-Reply-To: <1a2.d132280.2b24ba49@aol.com> References: <1a2.d132280.2b24ba49@aol.com> X-Mailer: VM 7.07 under 21.5 (beta6) "bok choi" XEmacs Lucid Tomato: Heliotrope Sender: cat-dist@mta.ca Precedence: bulk Topos8@aol.com writes: > I've been reading Lawvere's 1970 paper "Equality in hyperdoctrines and > comprehension schema...." which appeared in the AMS series Symposia in Pure > Mathematics, volume 17, pp 1-14. > > In the first line on page 12 he refers to the " 'twisted morphism category' " > B^ and the forgetful functor from B^ to (B op) x (B). Objects of B^ are morphisms (f:a->b) of B. Morphism from (f:a->b) to (g:c->d) in B^ is a pair of morphisms ((p:c->a),(q:b->d)), forming together with f and g commuting square (note the direction of arrows). Alternatively, one can define 'twisted morphism category' as Grotendieck construction for Hom functor: Hom: B^op x B -> Set. > > Can someone explain what this twisted morphism category is and/or provide a > reference to the definition? > > Thanks for your help. > > Carl Futia > Nikita. > > 9-Dec-2002 17:04:22 -0400,3582;000000000000-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 09 Dec 2002 17:04:22 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18LUvV-0006vG-00 for categories-list@mta.ca; Mon, 09 Dec 2002 16:54:53 -0400 Message-Id: <200212091900.LAA28546@coraki.Stanford.EDU> X-Mailer: exmh version 2.1.1 10/15/1999 To: categories@mta.ca Subject: categories: Re: concatenation Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Mime-Version: 1.0 Content-Transfer-Encoding: quoted-printable Date: Mon, 09 Dec 2002 11:00:39 -0800 From: Vaughan Pratt Sender: cat-dist@mta.ca Precedence: bulk >From: "Al Vilcius" >concatenation of lists and streams from an alphabet A: >- formally given by the unique arrow to a terminal coalgebra >- heuristically it is supposed to be thought of as =93erasing the comma=94= = between a >pair of streams (a,b) >But how is this to be understood computationally? I'm unclear as to the benefits if any of addressing Al's concern in the context of coalgebras, or of anything to do with categories for that matt= er. Forgetting for the moment any effectiveness that might be implicit in the= notion of "stream", the underlying structures here become accessible to a broader audience when presented as labeled chains (linear orders), call= these lists, with the list members being the labels. The concatenation o= f a linearly ordered family of lists is their marked union (with the family= 's index set providing the marks), augmented to a linear order in the eviden= t way (formally, dependent lexicographic product). With regard to effectiveness, I would expect Al's intuitions to be satisf= ied by defining the effective part eff(L) (or fin(L) for finite) of a list L as the sublist consisting of those elements having only finitely many predecessors, necessarily a prefix of L. So for example eff(N) =3D eff(N @ L) =3D N eff(Z) =3D eff(R) =3D eff(Z @ [3,1,4]) =3D [] eff(R+) =3D [0] eff([3,1,4] @ Z) =3D [3,1,4] eff(eff(L)) =3D eff(L) eff(L @ M) =3D L @ eff(M) if eff(L) =3D L =3D eff(L) otherwise eff(L @ M) =3D eff(L @ eff(M)) but not eff(L @ M) =3D eff(eff(L) @ eff(M)) where L,M are any lists, N,Z,R,R+ are the lists of natural numbers, integers, reals, and nonnegative reals standardly ordered, @ (McCarthy's MLISP notation c.1959 for APPEND) is binary concatenation, and [a,b,c] parallels set theory's {a,b,c}. The n-th element (n in N) of L is define= d for L iff it is defined for eff(L). The head of a list is its first elem= ent, the tail is the sublist that omits just the head, and the domain of both head and tail consists of those lists with nonempty effective part. Al's example of the concatenation of the list of positive odd integers wi= th the reverse of the list of even such then has as its effective part just the positive odd integers. Let me hasten to add that I am not here raising any objection to coalgebr= aic notions of concatenation in the context of an overall coalgebraic framewo= rk, where considerations of uniformity fully justify the use of coalgebraic definitions throughout. For the purposes of answering Al's question howe= ver, uniformity merely for its own sake has the potential to become an obstacl= e to understanding such an elementary issue, at least for those not already= thoroughly steeped in the coalgebraic method. Vaughan Pratt 9-Dec-2002 17:04:22 -0400,2859;000000000000-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 09 Dec 2002 17:04:22 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18LUuy-0006tO-00 for categories-list@mta.ca; Mon, 09 Dec 2002 16:54:20 -0400 Message-ID: From: "S.J.Vickers" To: categories@mta.ca Subject: categories: RE: concatenation Date: Mon, 9 Dec 2002 15:54:25 -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 Al Vilcius asks: > concatenation of lists and streams from an alphabet A: > - formally given by the unique arrow to a terminal coalgebra > - heuristically it is supposed to be thought of as "erasing > the comma" between a > pair of streams (a,b) > > But how is this to be understood computationally? > eg. write down all the +ve odd integers and then all the even ones in reverse > order to get a stream (1, 3, 5, .........., 6, 4, 2) > can this be made into a stream specification? > ie. what is the behaviour of the "dots" in the middle? I don't have the Rutten paper. However, if it says what I expect then the idea is this. A coalgebra X -> 1 + AxX says how an element of X is either empty or can have an atom (from A) pulled off it on the left - in other words, it is a "cons" of a head atom and a tail sequence. Hence an element of X can either have just finitely many atoms pulled off it before it's exhausted, or it can supply infinitely many atoms. This gives the map from X to a final coalgebra A* comprising the finite and countably infinite sequences. The infinite sequences are infinite on the right, not the left, so 1, 3, 5, ... is one, but not ..., 6, 4, 2. The map A*xA* -> 1 + Ax(A*xA*) shows how to pull a head off a pair (s,t) of sequences. If s is non-empty, then take its head. If s is empty, take the head of t. If both are empty then there is no head (so map to the element of 1). The concatenation map A*xA* -> A* therefore acts as follows: if s is finite, then (s,t) maps to (elements of s followed by elements of t) - you pull all the elements of s off, and then when you've finished you start on t. if s is infinite, then (s,t) maps to s. You never finish taking the elements off s. Thus the concatenation question has a simple but boring answer. 1, 3, 5, ... concatenated with anything is just 1, 3, 5, ... again. And this is exactly what will happen if you compute the answer in a lazy programming language with lists, such as Haskell. Steve Vickers Department of Pure Maths Faculty of Maths and Computing The Open University ----------- Tel: 01908-653144 Fax: 01908-652140 Web: http://mcs.open.ac.uk/sjv22 10-Dec-2002 20:57:12 -0400,1055;000000000000-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 10 Dec 2002 20:57:12 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18Lv1R-0000Ye-00 for categories-list@mta.ca; Tue, 10 Dec 2002 20:46:45 -0400 Date: Tue, 10 Dec 2002 01:34:51 -0500 (EST) From: Fred E J Linton Subject: categories: RE: twisted morphism category To: Categories Message-id: <02121006345179/0004142427DP2EM@mcimail.com> Content-transfer-encoding: 7BIT Sender: cat-dist@mta.ca Precedence: bulk The "twisted morphism category" arising from the category B is the category of "elements of" the set-valued hom-functor B^op x B ---> Sets of B . Its objects are the morphisms f: X ---> Y of B ; a map from f to g: X' ---> Y' is a pair of B-morphisms, x: X' ---> X , y: Y ---> Y' satisfying g = yfx . I certainly used that name in the mid or late '60s, in work I'm not able to cite you from here, sorry. Cheers, -- FEJ Linton 11-Dec-2002 19:20:36 -0400,4997;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 11 Dec 2002 19:20:36 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18MG4s-0005GX-00 for categories-list@mta.ca; Wed, 11 Dec 2002 19:15:42 -0400 Date: Wed, 11 Dec 2002 14:34:29 +0100 (MET) Message-Id: <200212111334.gBBDYTN19657@math.u-strasbg.fr> From: crans@math.u-strasbg.fr To: categories@mta.ca Subject: categories: PSSL 78 - Second announcement X-Antivirus: scanned by sophos at u-strasbg.fr MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: quoted-printable X-MIME-Autoconverted: from 8bit to quoted-printable by ns1.u-strasbg.fr id gBBDYTRW097242 Sender: cat-dist@mta.ca Precedence: bulk PERIPATETIC SEMINAR ON SHEAVES AND LOGIC (PSSL 78) Second Announcement Dear friends and colleagues, The 78th meeting of the PSSL will be held in Strasbourg over the weekend of 15-16 February 2003. As usual, we welcome talks on sheaves, category theory, logic and related areas. As the meeting is informal in nature talks on work in progress are also welcome.=20 Those wishing to attend the meeting are kindly asked to complete and return the registration form below. VENUE The meeting will be held at the Salle de Conf=E9rences of the Institut de Recherche Math=E9matique Avanc=E9e Unit=E9 Mixte de Recherche 7501 de l'Universit=E9 Louis Pasteur et du CNR= S 7 rue Ren=E9-Descartes 67084 Strasbourg France TRAVEL INFORMATION Strasbourg is the capital of Europe, and is located in the northeastern part of France, close to the French-German border. Strasbourg Airport has direct flights to and from a number of main European airports, and a bus-tram connection to the city centre. Strasbourg can also be reached through Basel-Mulhouse airport (train connection) and Frankfurt airport (Lufthansa bus connection). Because of its central location, there are also good train connections to and from Strasbourg, for example from Germany, Belgium and Italy. The IRMA can be reached from the station and from the city centre by taking tram line C direction "Esplanade" and getting off at the stop "Universit=E9s". It is then a short walk along rue Edmond Labb=E9, the building being on your left. ACCOMMODATION A hotel room will be reserved for you upon request, in one of the following hotels: Hotel Kleber ** Tel: +33 3 88 32 09 53 29 Place Kleber Fax: +33 3 88 32 50 41 67000 Strasbourg Email: hotel@hotel-kleber.com prices: single 39/51 euros, double 45/58 euros, breakfast 5.50 euros H=F4tel aux Trois Roses ** Tel: +33 3 88 36 56 95 7 rue de Zurich Fax: +33 3 88 35 06 14 67000 Strasbourg Email: info@hotel3roses-strasbourg.com prices: single 45 euros, double 61 or 69 euros, breakfast 6 euros H=F4tel de l'Esplanade ** Tel: +33 3 88 61 38 95 1 Boulevard Leblois Fax: +33 3 88 60 66 87 67000 Strasbourg Email: hotel.esplanade@wanadoo.fr prices: single 46 euros, double 49 euros, breakfast 5.50 euros or in one of the many other hotels in Strasbourg. Hotel Kleber is in the city centre, the other two mentioned are within easy walking distance of the Institute. SCHEDULE On Friday evening I suggest we will meet at 20.00 h at Penjab, 12 rue des Tonneliers, tel +33 3 88 32 36 37, reputedly the best Indian restaurant in Strasbourg. It is located near the tram A&D stop "Langstross Grand'Rue". On Saturday morning talks will start at 9.00 h. On Sunday the last talk will end at 12.30 h. PARTICIPANTS The following people have already indicated their willingness to give a talk: Pierre Ageron (Universit=E9 de Caen) Philippe Gaucher (Universit=E9 Louis Pasteur et CNRS) Marino Gran (Universit=E9 du Littoral C=F4te d'Opale) Rudger Kieboom (Vrije Universiteit Brussel) J=FCrgen Koslowski (Technische Universit=E4t Braunschweig) Tim van der Linden (Vrije Universiteit Brussel) Jir=ED Rosick=FD (Masaryk University) WEB PAGE A web page for the meeting containing relevant links and regularly updated information is located at http://www-irma.u-strasbg.fr/~crans/pssl78/ Looking forward to seeing you here in Strasbourg, Sjoerd Crans (crans@math.u-strasbg.fr) ------------------------------------------------------- PSSL 78 Registration Form Name: Affiliation: Address: Email: I wish to attend the 78th meeting of the PSSL to be held in Strasbourg over the weekend of 15-16 February 2003. I do/do not* wish to give a talk of 25/40* min. The title will be: Please do/do not* reserve accommodation for me. I need a single/double* room. I will arrive on Thursday 13/Friday 14/Saturday 15* February and I will depart on Sunday 16/Monday 17/Tuesday 18* February. *Delete if inappropriate. ------------------------------------------------------- 12-Dec-2002 11:53:14 -0400,1560;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 12 Dec 2002 11:53:14 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18MVR4-0002Cf-00 for categories-list@mta.ca; Thu, 12 Dec 2002 11:39:38 -0400 Date: Wed, 11 Dec 2002 09:46:21 -0500 (EST) From: James Stasheff X-X-Sender: stasheff@login1.isis.unc.edu To: Categories Subject: categories: Re: twisted morphism category In-Reply-To: <02121006345179/0004142427DP2EM@mcimail.com> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Yikes! is everything these days `twisted' some even refer to a simple regrading as a twist .oooO Jim Stasheff jds@math.unc.edu (UNC) Math-UNC (919)-962-9607 \ ( Chapel Hill NC FAX:(919)-962-2568 \*) 27599-3250 http://www.math.unc.edu/Faculty/jds On Tue, 10 Dec 2002, Fred E J Linton wrote: > The "twisted morphism category" arising from the category B is the > category of "elements of" the set-valued hom-functor B^op x B ---> Sets > of B . Its objects are the morphisms f: X ---> Y of B ; a map from > f to g: X' ---> Y' is a pair of B-morphisms, x: X' ---> X , > y: Y ---> Y' satisfying g = yfx . I certainly used that name in the > mid or late '60s, in work I'm not able to cite you from here, sorry. > > Cheers, > > -- FEJ Linton > > > > 12-Dec-2002 17:36:34 -0400,1959;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 12 Dec 2002 17:36:34 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18Mas7-0005n2-00 for categories-list@mta.ca; Thu, 12 Dec 2002 17:27:55 -0400 Message-ID: <3DF77BA0.F5B029F4@bangor.ac.uk> Date: Wed, 11 Dec 2002 17:53:36 +0000 From: Ronnie Brown X-Mailer: Mozilla 4.79 [en] (Win98; U) X-Accept-Language: en MIME-Version: 1.0 To: "categories@mta.ca" Subject: categories: Preprint: Cubical abelian groups with connections are equivalent to chain complexes Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Cubical abelian groups with connections are equivalent to chain complexes Ronald Brown and Philip J. Higgins Abstract: The theorem of the title is deduced from the equivalence between crossed complexes and cubical $\omega$-groupoids with connections proved by the authors in 1981. In fact we prove the equivalence of five categories defined internally to an additive category with kernels. Available as math.AT/0212157 and as http://www.bangor.ac.uk/~mas010/cubabgp3.pdf -- Professor Emeritus R. Brown, School of Informatics, Mathematics Division, University of Wales, Bangor Dean St., Bangor, Gwynedd LL57 1UT, United Kingdom Tel. direct:+44 1248 382474|office: 382681 fax: +44 1248 361429 World Wide Web: home page: http://www.bangor.ac.uk/~mas010/ (Links to survey articles: Higher dimensional group theory Groupoids and crossed objects in algebraic topology) Raising Public Awareness of Mathematics CDRom Version 1.1 http://www.bangor.ac.uk/~mas010/CDadvert.html Symbolic Sculpture and Mathematics: http://www.cpm.informatics.bangor.ac.uk/sculmath/ Centre for the Popularisation of Mathematics http://www.cpm.informatics.bangor.ac.uk/ 16-Dec-2002 14:20:56 -0400,2360;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 16 Dec 2002 14:20:56 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18NzhX-0007B2-00 for categories-list@mta.ca; Mon, 16 Dec 2002 14:10:47 -0400 Message-ID: <3DFDE0B1.B77218F3@bangor.ac.uk> Date: Mon, 16 Dec 2002 14:18:25 +0000 From: Ronnie Brown X-Mailer: Mozilla 4.79 [en] (Win98; U) X-Accept-Language: en MIME-Version: 1.0 To: "categories@mta.ca" Subject: categories: Preprint: Crossed complexes and homotopy groupoids ... Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Comments welcome on the following survey: Ronald Brown Crossed complexes and homotopy groupoids as non commutative tools for higher dimensional local-to-global problems Abstract: (This is an extended account of a lecture given at the meeting on `Categorical Structures for Descent and Galois Theory, Hopf Algebras and Semiabelian Categories', Fields Institute, September 23-28, 2002.) We outline the main features of the definitions and applications of crossed complexes and cubical \omega-groupoids with connections. These give forms of higher homotopy groupoids, and new views of basic algebraic topology and the cohomology of groups, with the ability to obtain non commutative results and compute homotopy types. (27 pages, 81 references) http://www.informatics.bangor.ac.uk/public/mathematics/research/preprints/02/algtop02.html#02.26 http://www.bangor.as.uk/~mas010/fields-art3.pdf -- Professor Emeritus R. Brown, School of Informatics, Mathematics Division, University of Wales, Bangor Dean St., Bangor, Gwynedd LL57 1UT, United Kingdom Tel. direct:+44 1248 382474|office: 382681 fax: +44 1248 361429 World Wide Web: home page: http://www.bangor.ac.uk/~mas010/ (Links to survey articles: Higher dimensional group theory Groupoids and crossed objects in algebraic topology) Raising Public Awareness of Mathematics CDRom Version 1.1 http://www.bangor.ac.uk/~mas010/CDadvert.html Symbolic Sculpture and Mathematics: http://www.cpm.informatics.bangor.ac.uk/sculmath/ Centre for the Popularisation of Mathematics http://www.cpm.informatics.bangor.ac.uk/ 16-Dec-2002 14:20:57 -0400,2371;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 16 Dec 2002 14:20:57 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18Nzi9-0007DK-00 for categories-list@mta.ca; Mon, 16 Dec 2002 14:11:25 -0400 To: categories@mta.ca Subject: categories: Internal logic of lex categories From: Andrej Bauer Date: 16 Dec 2002 18:56:12 +0100 Message-ID: Lines: 49 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 I seem to remember that some years ago at MFPS conference in Pittsburgh, Peter Freyd gave a talk on the internal logic of lex categories. Is this correct, and if so, has it been written down? It's probably easy to explain the gist of the talk, so if it has not been written down, perhaps someone with a memory better than mine can tell us what Freyd said. (Insert remarks about horse's mouth here.) Here is an attempt at reconstructing the logic. We want a logic that can be interpreted in any category C with finite limits, and we want a suitable completeness theorem, i.e., the semantics in lex categories is complete. Since C has pullbacks, Sub(A) has finite limits for any A. This means we should have the logical constant truth T and conjunction: T phi and psi Since there are equalizers in C, we should also allow equality (at each type A): t =_A u So now the question is what else is needed. We're not done yet since, semantically speaking, we have axiomatized equalizers and only pullbacks of monos along monos. Presumably we have to axiomatize the terminal object: 1 type ("1 is a type") * : 1 ("* is an element of 1") t =_1 * ("every element of 1 is equal to *") This still isn't enough because we don't have general pullbacks, or is it? I suspect we need not worry about binary products because the syntactic model will have them "for free". What did Peter Freyd say about this? Andrej Bauer Deptatment of Mathematics and Physics University of Ljubljana Slovenia http://andrej.com/ 16-Dec-2002 17:26:10 -0400,1208;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 16 Dec 2002 17:26:10 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18O2fA-0003iX-00 for categories-list@mta.ca; Mon, 16 Dec 2002 17:20:32 -0400 Date: Mon, 16 Dec 2002 14:53:34 -0500 (EST) From: Peter Freyd Message-Id: <200212161953.gBGJrYx0010235@saul.cis.upenn.edu> To: categories@mta.ca Subject: categories: Re: Internal logic of lex categories Sender: cat-dist@mta.ca Precedence: bulk Andrej asks I seem to remember that some years ago at MFPS conference in Pittsburgh, Peter Freyd gave a talk on the internal logic of lex categories. Is this correct, and if so, has it been written down? It's probably easy to explain the gist of the talk, so if it has not been written down, perhaps someone with a memory better than mine can tell us what Freyd said. (Insert remarks about horse's mouth here.) The horse's work has moved from mouth to print: Cartesian logic. Theoret. Comput. Sci. 278 (2002), no. 1-2 The slogan is that the logic of unique existential quantification is the logic of cartesian categories. 16-Dec-2002 17:26:11 -0400,1564;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 16 Dec 2002 17:26:11 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18O2eO-0003eT-00 for categories-list@mta.ca; Mon, 16 Dec 2002 17:19:44 -0400 X-Sender: cxm7/pop.cwru.edu@localhost (Unverified) X-Mailer: QUALCOMM Windows Eudora Version 5.2.0.9 Date: Mon, 16 Dec 2002 14:25:10 -0500 To: categories@mta.ca From: Colin McLarty Subject: categories: Re: Internal logic of lex categories In-Reply-To: Mime-Version: 1.0 Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Hi, I gave a correct syntax for lex logic, and a completeness theorem, in "Left exact logic", Journal of Pure and Applied Algebra, 41 (1986) 63-66. The point is, that you must be able assert existence (that is, existence of a value in some equalizer sort) conditional on equations. So you need sequents with equations on the the lefthand side. And of course you could do it all as a term logic with only conjunctions of equations as formulas, or with just atomic formulas and sequences with lists of atomic formulas on both sides. In fact, you can radically shorten the lefthand sides by a trick I explain in exercises 21-23 of chapter 20 of ELEMENTARY CATEGORIES, ELEMENTARY TOPOSES. the point of that is that, by looking at the righthand side, you can tell what equations are required as presuppositions, and suppress them. best, Colin 17-Dec-2002 19:04:30 -0400,1619;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 17 Dec 2002 19:04:30 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18OQfV-0005AU-00 for categories-list@mta.ca; Tue, 17 Dec 2002 18:58:29 -0400 Date: Mon, 16 Dec 2002 21:49:42 +0000 (GMT) From: "Prof. Peter Johnstone" To: categories@mta.ca Subject: categories: Re: Internal logic of lex categories In-Reply-To: Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Scanner: exiscan for exim4 (http://duncanthrax.net/exiscan/) *18O37O-0000Kx-00*gD1ts4keQxE* Sender: cat-dist@mta.ca Precedence: bulk On 16 Dec 2002, Andrej Bauer wrote: > > I seem to remember that some years ago at MFPS conference in > Pittsburgh, Peter Freyd gave a talk on the internal logic of lex > categories. Is this correct, and if so, has it been written down? It's > probably easy to explain the gist of the talk, so if it has not been > written down, perhaps someone with a memory better than mine can tell > us what Freyd said. (Insert remarks about horse's mouth here.) > Someone ought to contribute the name of Michel Coste to this discussion, since he produced a perfectly serviceable syntax for cartesian logic over twenty years before Peter Freyd, and ten years before Colin McLarty. His version was published in SLNM 753 (the proceedings of the 1977 Durham Symposium on Applications of Sheaves). Peter Johnstone 17-Dec-2002 19:04:31 -0400,906;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 17 Dec 2002 19:04:31 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18OQit-0005Lh-00 for categories-list@mta.ca; Tue, 17 Dec 2002 19:01:59 -0400 Message-ID: <20021217193631.10836.qmail@web12008.mail.yahoo.com> Date: Tue, 17 Dec 2002 11:36:31 -0800 (PST) From: Andrei Popescu To: categories@mta.ca MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Sender: cat-dist@mta.ca Precedence: bulk Dear Sir or Madame, I am Andrei Popescu, junior scientist at the University of Bucharest, Romania. I dear to ask for your help in the following matter: does there exist any characterization of the projective objects in the category of all the algebras of a given (arbitrary) signature? Thank you very much. Respectfully, Andrei 17-Dec-2002 19:04:31 -0400,5776;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 17 Dec 2002 19:04:31 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18OQi2-0005J6-00 for categories-list@mta.ca; Tue, 17 Dec 2002 19:01:06 -0400 Date: Tue, 17 Dec 2002 13:19:34 +0100 (MET) From: Taylor Paul Message-Id: <200212171219.gBHCJY7w012042@pianeta.di.unito.it> To: categories@mta.ca Subject: categories: Re: internal logic for lex categories X-AntiVirus: Scanned for viruses by VirusFinder @2001-tecnici@di.unito.it - Email Clean Sender: cat-dist@mta.ca Precedence: bulk Andrej Bauer asked about the INTERNAL LOGIC OF LEX CATEGORIES. He gave a sketch of such a logic, based primarily on EQUALITY. Another conspicuous feature is the SYMMETRY in the notions of equality, conjunction, product and pullback. The reason for being interested in such a logic is presumably in order to give interpretations of "generalised", "dependent-type" or "essentially" algebraic theories. The theory of categories is the leading example of this, the TYPE Hom(x,y) being dependent on the TERM-variables x and y. I would argue that lex categories are the WRONG structure in which to interpret such theories. SEMANTICALLY, there are lots of interesting categories (of domains, of locally compact spaces, of differentiable manifolds, and so on) that don't have all finite limits, but in which one would nevertheless like to interpret such theories. What, for example, is a locally compact topological groupoid? SYNTACTICALLY, equations conditional on equations are not how we think about, for example, composition in categories. When we are about to form "f;g", we already know that the target of f is the same object as the source of g - it is not an accidental situation whose validity we have to test "on the fly". (This point was made, using Kant's synthetic/analytic distinction, by John Cartmell in his treatment of generalised algebraic theories in JPAA in 1986.) Mathematicians have, traditionally, not bothered about such issues - "either the objects are equal or they're not" - but in a computational setting, it becomes significant if this equality needs to be tested "at run time". Proof theory also distinguished between INTENSIONAL and EXTENSIONAL equality. Generalised algebraic theories come first, equality is an add-on. In particular, we need to give account of the more basic syntactic notion of SUBSTITUTION. This is interpreted by pullback, but is by no means symmetric between the two legs: one is the term containing the free variable, the other the term to be substituted. On the semantic side, pullback often encodes INVERSE IMAGE, which is also asymmetrical. For example, in topology we use inverse images of OPEN subspaces and maps along ARBITRARY continuous functions. It was to capture this situation (specifically, in categories of domains) that I introduced CATEGORIES WITH DISPLAY MAPS in my 1987 PhD thesis (and earlier in CTCS1, LNCS 240). A class of display maps is simply one that is closed under pullback along any map in the category. I use an open-triangle arrowhead for such maps. Syntactically, a display map is a map between contexts that simply omits one (the last) typed variable: Gamma, z:Z ----|> Gamma This corresponds to WEAKENING in type theory. An arbitrary map Delta = [y1:Y1, ..., ym:Ym] ----> Gamma = [x1:X1, ..., xn:Xn] in this category assigns a term ai:Xi, possibly involving the ys, for each position in the target context. Pullback of the display map along this map substitutes these terms for the xs in the type Z, which may have depended on these variables. Terms of type Z in context Gamma are splittings of the display; these undergo substitution in the same way when we pull the splittings back along Delta->Gamma. You may think that, given a highly dependent system of types, this category (the CLASSIFYING CATEGORY or CATEGORY OF CONTEXTS AND SUBSTITUTIONS) would be complicated to construct. Indeed it is, if you approach it in the wrong way, as a huge structural recursion. But this is because, as functional programmers know very well, recursion does not interact well with associativity. There is, in fact, an EASY AND UNIFORM CONSTRUCTION of the category from ANY TYPE THEORY that has all of the usual structural rules, in particular weakening (so this doesn't apply to linear logic). However, we obtain the category via an (elementary) SKETCH: - the objects are contexts, - the morphisms are GENERATED from two classes: - display maps (weakening by a typed variable) and - their splittings (cut with a typed term). - the equations are (those of the theory) plus five more, of which the well known SUBSTITUTION LEMMA is the most complicated. The place to look for the details of this is not my thesis, but CHAPTER VIII of my book, "Practical Foundations of Mathematics" Cambridge University Press, 1999 http://www.dcs.qmul.ac.uk/~pt/book/html/c8.html As I said, I introduced display maps in my thesis for domain theory, and in particular to discuss dependent products (polymorphism). The point was that NOT ALL SUCH PRODUCTS EXIST, as they do in Set, for which Lawvere had introduced the notion of HYPERDOCTRINE. As I was interested in constructing dependent products in semantic categories, it was important to seek ways of simplifying the calculations as much as possible. Ultimately, I found that only the special case of so-called PARTIAL PRODUCTS was needed. This reduction is in Section 9.4 of the book. The rest of Chapter IX deals with other aspects of type theories. Paul Taylor 17-Dec-2002 19:04:31 -0400,3589;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 17 Dec 2002 19:04:31 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18OQhB-0005GF-00 for categories-list@mta.ca; Tue, 17 Dec 2002 19:00:13 -0400 Subject: categories: Re: Internal logic of lex categories References: Reply-To: Andrej Bauer To: categories@mta.ca From: Andrej Bauer Date: 16 Dec 2002 23:36:07 +0100 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 Message-Id: I think I can answer my own question: it's enough to have conjunction, truth, and equations to get a complete semantics of lex categories. This really is just an exercise in categorical logic. Sorry for bothering everyone with it. We work over multi-sorted type theory. The basic judgments are 1) term t has type B in typing context x_1:A_1,...,x_n:A_n: x_1:A_1,...,x_n:A_n | t : B 2) phi is a formula in context x_1:A_1,...x_n:A_n x_1:A_1,...,x_n:A_n | phi 3) assumptions psi_1,...,psi_k logically entail phi: x_1:A_1,...,x_n:A_n | psi_1,...,psi_k |- phi Formulas are built from equality, truth, and conjunction. The syntactic model is built as follows: - OBJECTS are formulas in contexts x_1:A_1, ..., x_n:A_n | phi where A_i are types, x_i are distinct variables, and phi is a formula built from truth T, conjunction and equations. The variables appearing in phi must be listed in the context. Two formulas in contexts which only differ in the names of variables are considered equal. - MORPHISMS: let Gamma be the context x_1:A_1, ..., x_n:A_n and Delta the context y_1:B_1, ..., y_m:B_m. A morphism t Gamma|phi -------> Delta|psi is an m-tuple of terms t = , where the type of t_i in context Gamma is B_i, written as Gamma | t_i : B_i, such that the following is provable: Gamma | phi and (y_1 = t_1) and ... and (y_m = t_m) |- psi In words, the assumption phi together with the assumptions y_1 = t_1, ..., y_m = t_m logically entail psi. Composition is defined by substitution. The identity morphism on Gamma|phi is the tuple . Morphisms are quotiented modulo provable equality. More precisely, morphisms t Gamma|phi -------> Delta|psi and s Gamma|phi -------> Delta|psi are considered provably equal if the following entailment is provable, for every i = 1,...,m: Gamma | phi |- t_i = s_i This probably does the job, i.e., the syntactic model is a category with finite limits and is universal such category. The product of objects Gamma | phi and Delta | psi is the product Gamma, Delta | phi and psi where the contexts Gamma and Delta are presumed to list disjoint sets of variables (this can always be achieved by renaming). The equalizer of ---t---> Gamma|phi Delta|psi ---s---> is the object Gamma | phi and (t_1 = s_1) and ... and (t_m = s_m) with the obvious inclusion into Gamma|phi. I think this does the job. Andrej 18-Dec-2002 11:59:17 -0400,1421;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 18 Dec 2002 11:59:17 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18OgUc-0001QE-00 for categories-list@mta.ca; Wed, 18 Dec 2002 11:52:18 -0400 Date: Wed, 18 Dec 2002 09:15:26 +0000 (GMT) From: "Prof. Peter Johnstone" To: categories@mta.ca Subject: categories: Re: Internal logic of lex categories In-Reply-To: Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Scanner: exiscan for exim4 (http://duncanthrax.net/exiscan/) *18OaIe-0006Ck-00*Unm9XVjKwBY* Sender: cat-dist@mta.ca Precedence: bulk On 16 Dec 2002, Andrej Bauer wrote: > I think I can answer my own question: it's enough to have conjunction, > truth, and equations to get a complete semantics of lex categories. > This really is just an exercise in categorical logic. Sorry for > bothering everyone with it. > [CUT] > > I think this does the job. > Andrej > No, it doesn't: you need to include *some* existential quantification. In the syntax Andrej proposes, it's impossible to formulate the theory of categories (for the reason why this theory is a good test case, see Example D2.4.7 in "Sketches of an Elephant"). Peter Johnstone 18-Dec-2002 12:22:16 -0400,2720;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 18 Dec 2002 12:22:16 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18Oguq-00032m-00 for categories-list@mta.ca; Wed, 18 Dec 2002 12:19:24 -0400 Message-Id: <5.1.0.14.2.20021218073244.048b1ec0@imap-c.nd.edu> X-Sender: cmclarty@imap-c.nd.edu X-Mailer: QUALCOMM Windows Eudora Version 5.1 Date: Wed, 18 Dec 2002 09:07:12 -0500 To: categories@mta.ca From: Colin S McLarty Subject: categories: Re: Internal logic of lex categories References: Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii"; format=flowed Sender: cat-dist@mta.ca Precedence: bulk At 09:49 PM 12/16/02 +0000, Peter Johnstone wrote: >Someone ought to contribute the name of Michel Coste to this discussion, >since he produced a perfectly serviceable syntax for cartesian logic >over twenty years before Peter Freyd, and ten years before Colin McLarty. >His version was published in SLNM 753 (the proceedings of the 1977 >Durham Symposium on Applications of Sheaves). It is serviceable. But it has an unusual feature, as well-formedness of a formula depends on provability of other formulas. You must define the formulas and the theorems together. In the paradigm case of lex axioms for a category: Coste's version allows a formula "there is an arrow h, composite of f and g" only if the context proves "the codomain of f is the domain of g". The key point, to me, is that lex theories should NOT bother with an existential quantifier, unique or otherwise. Existence in these theories just means some equation is satisfied. So just use equations. Instead of saying "there is an arrow h composite of f and g" you should just talk about the composite gf, and when needed you recall that this presupposes "dom(g)=cod(f)". So, as the paradigm, the category axioms are simply: (1_A)f=f f(1_A)=f f(gh)=(fg)h where the composite terms (1_A)f and (gh) and so on, are understood as partially defined. The syntax for this logic is a standard sequent calculus. the formulas are only equations. Sequents have only single formulas on the righthand side. The rules are substitution, equality, and cut rule with the understanding that if you cut a formula with a composite term in it then you must add the presupposition of that term to the lefthand side of the resulting sequent. These are complete for the obvious interpretation in any left exact category (arrows defined on equalizers correspond to term-forming operators with presuppositions, where the presupposition is the equation of the equalizer). 18-Dec-2002 14:45:54 -0400,3518;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 18 Dec 2002 14:45:54 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18OjA6-0003Tr-00 for categories-list@mta.ca; Wed, 18 Dec 2002 14:43:18 -0400 Date: Wed, 18 Dec 2002 17:21:04 GMT Message-Id: <200212181721.gBIHL4kR003827@lime.comlab.ox.ac.uk> X-Authentication-Warning: lime.comlab: jg set sender to jg@lime.comlab using -f From: Jeremy Gibbons To: categories@mta.ca Subject: categories: The Fun of Programming Sender: cat-dist@mta.ca Precedence: bulk Dear colleagues: We would like to advertise the following symposium, and are pleased to invite you to participate. We apologize if you receive multiple copies of this announcement. Jeremy and Oege * THE FUN OF PROGRAMMING A symposium in honour of Professor Richard Bird's 60th birthday Examination Schools, Oxford 24th and 25th March 2003 Professor Richard Bird is well known for his contributions to functional programming: for his two textbooks, his "Functional Pearls" column in the Journal of Functional Programming, his work on synthesizing programs from specifications, his influence in the design of the language Haskell and its predecessors, and so on. This symposium is to celebrate Richard Bird's work on the occasion of his sixtieth birthday. The symposium will coincide with the publication by Palgrave of an eponymous book. This book is intended as much as a textbook for an advanced course in functional programming as it is a festschrift; its twelve chapters cover applications (pretty printing, musical composition, hardware description, graphical design) and techniques (the design of efficient data structures, interpreters for little languages, program testing and optimization) in functional programming. The contributors to the book will give short lectures at the symposium, and every participant at the symposium will receive a copy of the book. The symposium will take place from 10.30am on Monday 24th March 2003 to 4pm on Tuesday 25th, in Oxford's historical Examination Schools. The registration fee includes participation, buffet lunch and tea and coffee on both days, a formal dinner on the Monday night in Worcester College, and a copy of the book. There is a lower price for early registration; the capacity of the lecture room is limited and offered on a first-come first-served basis, so early registration is recommended. The speakers are as follows: Chris Okasaki (West Point) John Hughes (Chalmers) Jeremy Gibbons (Oxford) Paul Hudak (Yale) Oege de Moor (Oxford) Simon Peyton Jones (Microsoft) Conal Elliott Mary Sheeran (Chalmers) Mike Spivey (Oxford) Ross Paterson (City) Philip Wadler (Avaya) Ralf Hinze (Bonn) For further details, including registration information, see the website at http://www.comlab.ox.ac.uk/oucl/research/areas/ap/fop/ In particular, there is an early registration deadline (with reduced fee) of 7th February 2003, and a late registration deadline of 7th March. Jeremy Gibbons and Oege de Moor (organizers) -- Jeremy.Gibbons@comlab.ox.ac.uk Oxford University Computing Laboratory, TEL: +44 1865 283508 Wolfson Building, Parks Road, FAX: +44 1865 273839 Oxford OX1 3QD, UK. URL: http://www.comlab.ox.ac.uk/oucl/people/jeremy.gibbons.html 18-Dec-2002 14:45:54 -0400,3138;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 18 Dec 2002 14:45:54 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18OjAS-0003UT-00 for categories-list@mta.ca; Wed, 18 Dec 2002 14:43:40 -0400 Date: Wed, 18 Dec 2002 12:23:33 -0500 (EST) From: Peter Freyd Message-Id: <200212181723.gBIHNXDG021668@saul.cis.upenn.edu> To: categories@mta.ca Subject: categories: on the logic of unique existentials Sender: cat-dist@mta.ca Precedence: bulk The first solution to the "logic of cartesian categories" (I insist that Descartes invented equalizers as much as he invented products) presented itself with the introduction of essentially algebraic theories in 1971. It's an exercise. But it was always clear to me -- long before 1971 --that unique existential quantification was the central feature. (Yes, of course you can avoid it in the same way you can avoid ordinary existential quantification. Skolem taught us that.) There's no question one can assert unique existentials using finite limits. (As a sample: given a couple of binary predicates P on objects A,B and Q on objects B,C (modeled by maps from P to A and B and from Q to B and C) the assertion that for all a,b such that aPb there's a unique c such bQc is equivalent to the assertion that the map Pullback[P -> B, Q -> B] -> P is an iso. The rules of inference for unique existential quantification is what I saw as the central question. I wrote in Cartesian Logic: Twenty-five years ago this writer started listing these rules. Their remarkable inelegance caused him to conclude that he was staring at one of the very reasons for category theory. The notion of a cartesian category is much simpler than that of cartesian syntax. The language of cartesian categories has permeated mathematics as a whole, even among those who are convinced that there is nothing worth noting in the theory of categories (the usefulness of a language does not, in fact, imply the usefulness of its associated theory) and there is no chance that cartesian syntax is going to do any such thing....The particular impetus that propelled the present effort arose from the necessity [in an attempt to formalize the semantics of "logical programming"] of getting a handle on the process of adjoining generic subobjects to objects in cartesian categories. [The 25 years ago referred to the very first NY topos seminar. The rules at that point were horrendous.] Yes, once the solution for the generic subobject is stated one doesn't need cartesian logic. But it's a useful tool to find the solution. So here's a challenge. Take an arbitrary cartesian category and an object C therein. Now adjoin a generic category structure to the object C (use the one-sorted "pure category" theory). What are the objects? Try it just for the free cartesian category on C, in other words, what's the free cartesian category on a category-object? What are its objects? And harder: what are its maps? 18-Dec-2002 14:45:54 -0400,2705;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 18 Dec 2002 14:45:54 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18OjAx-0003Vj-00 for categories-list@mta.ca; Wed, 18 Dec 2002 14:44:11 -0400 Date: Wed, 18 Dec 2002 17:28:38 +0000 (GMT) From: "Prof. Peter Johnstone" To: categories@mta.ca Subject: categories: Re: Internal logic of lex categories In-Reply-To: <5.1.0.14.2.20021218073244.048b1ec0@imap-c.nd.edu> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Scanner: exiscan for exim4 (http://duncanthrax.net/exiscan/) *18Ohzr-0000pr-00*PuajJlI6e8M* Sender: cat-dist@mta.ca Precedence: bulk On Wed, 18 Dec 2002, Colin S McLarty wrote: > At 09:49 PM 12/16/02 +0000, Peter Johnstone wrote: > >Someone ought to contribute the name of Michel Coste to this discussion, > >since he produced a perfectly serviceable syntax for cartesian logic > >over twenty years before Peter Freyd, and ten years before Colin McLarty. > >His version was published in SLNM 753 (the proceedings of the 1977 > >Durham Symposium on Applications of Sheaves). > > > It is serviceable. But it has an unusual feature, as well-formedness of a > formula depends on provability of other formulas. You must define the > formulas and the theorems together. In the paradigm case of lex axioms for > a category: Coste's version allows a formula "there is an arrow h, > composite of f and g" only if the context proves "the codomain of f is the > domain of g". > > The key point, to me, is that lex theories should NOT bother with an > existential quantifier, unique or otherwise. Existence in these theories > just means some equation is satisfied. So just use equations. > I don't see why it should be any more, or less, convenient to work in a calculus where you have to insert side arguments to justify the definedness of terms, than in one where you have to insert side arguments to justify the well-formedness of formulae. And I don't see why I should be forced to give up using existential quantifiers in contexts where it's natural to do so. The slogan "existence just means some equation is satisfied" is only true if you restrict yourself to languages without primitive predicates (other than equality); it is of course possible to do this in cartesian logic, but I don't see why I should be forced to do so, any more than I see why I should accept the classical logicians' restriction of doing without primitive function symbols (other than constants). Peter Johnstone 19-Dec-2002 12:13:12 -0400,1190;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 19 Dec 2002 12:13:12 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18P35C-0006rm-00 for categories-list@mta.ca; Thu, 19 Dec 2002 11:59:34 -0400 Message-Id: <200212182008.MAA10044@coraki.Stanford.EDU> X-Mailer: exmh version 2.1.1 10/15/1999 To: categories@mta.ca Subject: categories: Re: on the logic of unique existentials Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Date: Wed, 18 Dec 2002 12:08:01 -0800 From: Vaughan Pratt Sender: cat-dist@mta.ca Precedence: bulk >(I insist that Descartes invented equalizers as much as he invented products) Unique existence is embodied in the number 1. While it reasonable to conjecture that the numbers 2 and 3 both predate 1 in the historical development of human thought, it seems even more likely that the littlest positive integer was sent out to work in the fields eons before Archimedes rushed naked into that cold street crying "Eureka", and we know pretty much just how long that was before Descartes rushed out crying "Equalizers." Vaughan 19-Dec-2002 13:59:00 -0400,3084;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 19 Dec 2002 13:59:00 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18P4qy-0005qF-00 for categories-list@mta.ca; Thu, 19 Dec 2002 13:53:00 -0400 Message-ID: <3E01FC61.C9D8133D@bangor.ac.uk> Date: Thu, 19 Dec 2002 17:05:37 +0000 From: Ronnie Brown X-Mailer: Mozilla 4.79 [en] (Win98; U) X-Accept-Language: en MIME-Version: 1.0 To: "categories@mta.ca" Subject: categories: preprint: The fundamental groupoid of the quotient of a Hausdorff space... Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk New preprint: R. Brown and P.J. Higgins TITLE: The fundamental groupoid of the quotient of a Hausdorff space by a discontinuous action of a discrete group is the orbit groupoid of the induced action ABSTRACT: The main result is that the fundamental groupoid of the orbit space of a discontinuous action of a discrete group on a Hausdorff space which admits a universal cover is the orbit groupoid of the fundamental groupoid of the space. We also describe work of Higgins and of Taylor which makes this result usable for calculations. As an example, we compute the fundamental group of the symmetric square of a space. The main result, which is related to work of Armstrong, is due to Brown and Higgins in 1985 and was published in sections 9 and 10 of Chapter 9 of the first author's book on Topology (Ellis Horwood, 1988). This is a somewhat edited, and in one point (on normal closures) corrected, version of those sections. Since the book is out of print, and the result seems not well known, we now advertise it here. It is hoped that this account will also allow wider views of these results, for example in topos theory and descent theory. math.AT/0212271 http://www.informatics.bangor.ac.uk/public/mathematics/research/preprints/02/algtop02.html#02.25 http://www.bangor.ac.uk/~mas010/orbitgpdxx.pdf Other Information: 1) A previous announcement of fields-art3.pdf had a url of bangor.as.uk/~mas010/fields-art3.pdf instead of bangor.ac.uk 2. Our web sites on sculpture and knots have just been reorganised and given a new look by Mike Yates under an EPSRC grant. There are new animations, and navigation is much easier. Have a look! (see below) -- Professor Emeritus R. Brown, School of Informatics, Mathematics Division, University of Wales, Bangor Dean St., Bangor, Gwynedd LL57 1UT, United Kingdom Tel. direct:+44 1248 382474|office: 382681 fax: +44 1248 361429 World Wide Web: home page: http://www.bangor.ac.uk/~mas010/ (Links to survey articles: Higher dimensional group theory Groupoids and crossed objects in algebraic topology) Raising Public Awareness of Mathematics CDRom Version 1.1 Symbolic Sculpture and Mathematics: Centre for the Popularisation of Mathematics http://www.cpm.informatics.bangor.ac.uk/centre/index.html 20-Dec-2002 14:53:27 -0400,1780;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 20 Dec 2002 14:53:27 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18PS6X-0003Su-00 for categories-list@mta.ca; Fri, 20 Dec 2002 14:42:37 -0400 Mime-Version: 1.0 X-Sender: borceux@mail.math.ucl.ac.be (Unverified) Message-Id: X-Mailer: Eudora F5.0.1 Date: Fri, 20 Dec 2002 16:57:31 +0100 To: categories@mta.ca From: Francis Borceux Subject: categories: Rene Lavendhomme Content-Type: text/plain; charset="iso-8859-1" ; format="flowed" Content-Transfer-Encoding: quoted-printable X-MailScanner: Found to be clean Sender: cat-dist@mta.ca Precedence: bulk It is with great sadness that I announce the death of our colleague Rene Lavendhomme, which occured this Thursday 19 december, some days before his 74th birthday. He has produced nice pieces of mathematics in non-abelian cohomology, categorical logic and synthetic differential geometry. More recently, he published works on philosophy, poetry, psychanalysis and their relations with category theory, in particular topos theory. He founded the category theory group in Louvain-la-Neuve and has been the supervisor of numerous PH.D. thesis, including mine. He was a very friendly person with a constructively critical mind. =46rancis Borceux -- ******************************************* PLEASE NOTICE THE NEW E-MAIL ADDRESS ******************************************* =46rancis Borceux D=E9partement de Math=E9matique Universit=E9 Catholique de Louvain 2 chemin du Cyclotron 1348 Louvain-la-Neuve Begium phone +32 (0)10 473170 fax +32 (0)10 472530 e-mail borceux@math.ucl.ac.be 21-Dec-2002 12:30:28 -0400,5656;000000000000-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 21 Dec 2002 12:30:28 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18PmT7-0002Y9-00 for categories-list@mta.ca; Sat, 21 Dec 2002 12:27:17 -0400 To: categories@mta.ca Subject: categories: [CSL03] Call For Papers: Computer Science Logic 2003 Message-Id: From: csl03 Date: Sat, 21 Dec 2002 14:53:08 +0100 Sender: cat-dist@mta.ca Precedence: bulk [ We apologize for the inevitable multiple copies of this announcement. Please see the note on mailing lists at the end. ] [ There is a PostScript copy of this Call at http://www.logic.at/csl03/CSL03-cfp.ps for display on notice boards. ] First Call for Papers Annual Conference of the European Association for Computer Science Logic and 8th Kurt Goedel Colloquium CSL'03 & KGC 25 August afternoon - 30 August 2003, Vienna, Austria Computer Science Logic (CSL) is the annual conference of the European Association for Computer Science Logic (EACSL). The Kurt Goedel Colloquium (KGC) is the biennial conference of the Kurt Goedel Society (KGS). The joint conference is intended for computer scientists whose research activities involve logic, as well as for logicians working on issues significant for computer science. Suggested topics of interest include: automated deduction and interactive theorem proving; constructive mathematics and type theory; equational logic and term rewriting; fuzzy logic; modal and temporal logics; computational proof theory; linear logic; finite model theory; bounded arithmetic; logical aspects of computational complexity; higher order logic; logic programming and constraints; lambda and combinatory calculi; logical foundations of programming paradigms; model checking; specification, extraction and transformation of programs; categorical logic and topological semantics; game semantics; domain theory; database theory. A lecture, jointly invited by CSL'03 & KGC and ESSLLI (European Summer School in Logic Language and Information) will be given by Sergei Artemov (CUNY, USA) Additional invited lectures will be given by (tentative): Bruno Buchberger (Johannes Kepler University, Austria) Dov Gabbay (King's College London, England) Helmut Veith (Vienna University of Technology, Austria) Nikolai Vorobjov (University of Bath, England) Andrei Voronkov (University of Manchester, England) The following tutorials are planned: Verification of infinite state systems (Ahmed Bouajjani, University of Paris 7, France) Computational epsilon calculus (Georg Moser, University of Muenster, Germany, and Richard Zach, University of Calgary, Canada) Quantifier elimination (Nikolai Vorobjov, University of Bath, England) Winning strategies and controller synthesis (Igor Walukiewicz, University of Bordeaux, France) The proceedings of the conference will be published in the Springer Lecture Notes in Computer Science series. Submitted papers must describe work not previously published. They must not be submitted concurrently to another conference with refereed proceedings. Research that is already submitted to a journal may be submitted to CSL, provided that (a) the PC chair is notified in advance that this is the case, and (b) it is not scheduled for journal publication before the conference. Submissions authored or coauthored by members of the Programme Committee are not allowed. Papers should preferably be submitted either in LNCS format or in 12pt A4 format. Papers should not exceed 14 pages; full proofs may appear in a technical appendix which will be read at the reviewers' discretion. The title page must contain: title and authors; physical and e-mail addresses; identification of corresponding author, if not the first author; an abstract of no more than 200 words; a list of keywords. The key dates for the conference are: Submission: The submission process is in two stages, both with strict deadlines: 31 March 2003 for the title and abstract, and 7 April 2003 for the full text. Notification: 2 June 2003 Final copy due: 18 June 2003 Prospective authors should check the conference Web page for any subsequent changes to these dates. Further information on all aspects of the conference will be found on the conference Web page: http://www.logic.at/csl03/ Programme Committee: Matthias Baaz (chair) Arnold Beckmann Lev Beklemishev Maarten de Rijke Chris Fermueller Didier Galmiche Harald Ganzinger Erich Graedel Petr Hajek Martin Hyland Reinhard Kahle Helene Kirchner Daniel Leivant Johann Makowsky (co-chair) Jerzy Marcinkowski Franco Montagna Robert Nieuwenhuis Michel Parigot Jeff Paris Helmut Schwichtenberg Jerzy Tiuryn [ Note on mailing lists. The To: header in each copy of this message contains the entry in our mailing list to which it was sent. If you wish the entry to be removed from our list, or have any problem with the mail, please contact csl03+calls@logic.at . ] 26-Dec-2002 11:38:04 -0400,2431;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 26 Dec 2002 11:38:04 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18Ra0E-0002ry-00 for categories-list@mta.ca; Thu, 26 Dec 2002 11:32:54 -0400 Date: Mon, 23 Dec 2002 20:56:26 -0800 (PST) From: Bill Rowan Message-Id: <200212240456.gBO4uQ860637@transbay.net> To: categories@mta.ca Subject: categories: New mail list Sender: cat-dist@mta.ca Precedence: bulk Hello everyone, I have finally done what I said I would do a few years ago, and started up an email list, at yahoogroups, centered around Beck modules. (If A is an algebra in a variety V, then the category of Beck modules over A [and in V] is the category of abelian group objects in the comma category (V,A). At least, that is how category theorists define it. I have some other ideas about it that lead to an equivalent category.) There was some interest in such a list at the time, I think it was around 9 or 10 years ago. I have found managing my univalg list (for universal algebra) to be easy enough that I want to start this list also. The univalg list includes mostly universal algebraists, not all of whom are interested in things with a category-theoretic flavor. I am, however, inviting the members of that list to join this new one. To subscribe, send an email to beckmodules-subscribe@yahoogroups.com. I have set it up so that I have to approve any subscriptions, in order to avoid certain spammers who seem to have automated the process of subscribing. Your email address will be visible only to other members of the list. For the greatest access to the features of the group, you can get a yahoo id by going to http://groups.yahoo.com and registering. Or, if you have a yahoo id already, you can easily join the beckmodules group. The service is free, being supported by advertising which is tolerably nonintrusive. Possible topics for posts include the controversy about how best to define Beck modules, cohomology theories (such as Jon Beck explored in his thesis), the related theory of enveloping ringoids (which I introduced in my thesis), connections with universal algebra and commutator theory (invented by JDH Smith) and lots of other ideas that I probably never heard of but am looking forward to hearing about. Best regards, Bill Rowan 29-Dec-2002 17:03:56 -0400,4542;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 29 Dec 2002 17:03:56 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18SkVt-0006bk-00 for categories-list@mta.ca; Sun, 29 Dec 2002 16:58:25 -0400 Date: Mon, 23 Dec 2002 14:07:28 +0100 From: "Konferencja ETAPS'03" To: categories@mta.ca Subject: categories: ETAPS03 - grants Message-ID: <20021223140728.A3042@absurd.mimuw.edu.pl> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline User-Agent: Mutt/1.2.5.1i Sender: cat-dist@mta.ca Precedence: bulk We apologize if you receive multiple copies of this message. ********************************************************** *** ETAPS 2003 *** *** APRIL, 5-13, 2003 *** *** WARSAW, POLAND *** *** *** *** http://www.mimuw.edu.pl/etaps03/ *** ********************************************************** ============================================================================= EC GRANTS FOR YOUNG RESEARCHERS AND ETAPS GRANTS FOR PARTICIPATION ============================================================================= Important dates: Application: before January 31st, 2003 Notification: before February 15th, 2003 A grant from the European Commission, High-Level Scientific Conferences, has been approved for supporting the participation to the Conference of young researchers (up to the age of 35 years at the time of the conference) who are nationals of a Member State or an Associated State, and who are actively participating in one of the ETAPS 2003 main conferences or in a satellite event. The organizers offer additional limited support possibilities for ETAPS 2003 participants who are not eligible for the EC-HSC grants above. So, if you need some financial support, apply under the scheme described below. Financial support may cover (up to 100% of): - ETAPS main conferences and satellite events registration fees - travel expenses - subsistence and accommodation costs in Warsaw For applying, please send an e-mail to etaps03-grants@mimuw.edu.pl The email should contain the following information about the applicant: name, gender, birth date, nationality, current student/working position and affiliation, and contact information (email address, fax, postal address). Please also state duration and the planned dates of your stay in Warsaw for ETAPS 2003, as well as the character of participation in ETAPS 2003 (in particular: please indicate if you are an author or a co-author of an accepted paper at one of the main conferences, an author or a co-author of a presentation at one of the satellite workshops, tutorials, etc). Those who wish to apply for refund of travel costs must additionally send: - an estimate of travel expenses (with the above application), and - not later than March, 24th 2003, a copy of the ticket with explicitly stated cost of the ticket. In case the ticket does not contain an explicit cost, an invoice of the purchase of the ticket should be sent as well. The copy of the ticket or an invoice should be faxed at the number +4822-5544400. Please bring the originals with you to Warsaw. Eligible costs are the cheapest airfare in economy class, or a second class train ticket, or a bus ticket. Grant applicants should register at the web site of ETAPS 2003 , as all other participants. However, do not forget to mark that you're applying for support from ETAPS 2003 organizers, and refrain from paying the participation fees until we send you our decision concerning the support. If you apply for support to cover your registration and you are not granted this support, your registration fee will be calculated according to the date of your registration, and not that of your actual payment, as long as you pay the fee within 7 days after your application was rejected. In any case you should yourself take care of your hotel reservation. If you book your hotel using the service provided via the conference web page you should also pay the hotel deposit as required.