Date: Tue, 10 Dec 1996 10:22:33 -0400 (AST) Subject: my book: "Practical Foundations of Mathematics" Date: Mon, 9 Dec 1996 21:16:37 GMT From: Paul Taylor STOP PRESS --- see my web page for my new home telephone number Practical Foundations of Mathematics Paul Taylor to be published by Cambridge University Press http://www.dcs.qmw.ac.uk/~pt/book In the time this book has taken me to write, various friends of mine have had babies and sent them to school. I just hope someone thinks that it has been worth the effort. The emotional cost of trying to get these 500 pages finished has made me seriously reclusive, and I owe many friends and colleagues replies to letters and email, for which I would like to make a general and sincere apology. The news is that seven of the eight chapters are finished and ready to be sent to the copy editors at CUP. I would however very much like to get my colleagues' views on individual chapters, if you feel that you would like some reading matter for the yuletide vacation. Ideally I would like comments from *both* experts *and* students, as it is useful to find out what topics need better explanation. Chapter 8 is mostly there but has not been polished yet. Practical Foundations collects the methods of construction of the objects of twentieth century mathematics. Although it is mainly concerned with a framework essentially equivalent to intuitionistic ZF, the book looks forward to more subtle bases in categorical type theory and the machine representation of mathematics. Each idea is illustrated by wide-ranging examples, and followed critically along its natural path, transcending disciplinary boundaries between universal algebra, type theory, category theory, set theory and programming. The first three chapters will be essential reading for the design of courses in discrete mathematics and reasoning, especially for the ``box method'' of proof taught successfully to first year informatics students. Chapters 4, 5 and 7 are an introduction to categorical logic. Between the formal languages translations are provided which are fluent, teaching the student how to write vernacular proofs which are sound in formal logics. Chapter 6 is a new approach to term algebras, induction and recursion, which have hitherto only been treated either naively or with set theory. The final chapter proves in detail the equivalence of types and categories, in particular between generalised algebraic theories and categories with display maps. Students and teachers of computing, mathematics and philosophy will find this book both readable and of lasting value as a reference work. The titles of the chapters are as follows, though as they are not very informative, I have put a list of the section and subsection names on the web at http://www.dcs.qmw.ac.uk/~pt/book/index.html 1. First Order Reasoning 5. Limits and Colimits 2. Types and Induction 6. Algebras of Terms and Proofs 3. Posets and Lattices 7. Adjunctions 4. Cartesian Closed Categories 8. Dependent Types The whole book is 500 pages, which I suspect is rather more than any of you will be able to digest, but I would like chapters 2-8 to get some attention, as well as Section 1.1! For this reason I would like to invite you to choose a *chapter* to read, and email me with your postal address. A well annotated chapter gets a draft copy of the whole book. Please try to return your comments by email or post by mid-January; of course this deadline will slip, but it is a vain attempt at self-discipline. Finally, several people have asked me what "position" I have at QMW. The answer is -- a desk, courtesy of Edmund Robinson. No more, no less. I have an Advanced Research Fellowship until the end of September 1997, am paid by the EPSRC (research council) and am still employed by Imperial College. Paul Taylor Date: Fri, 13 Dec 1996 00:15:51 -0400 (AST) Subject: chapters of my book Date: Thu, 12 Dec 1996 21:47:27 GMT From: Paul Taylor I would like to thank the almost thirty people who have offered to read chapters of my book over the vacation. I believe I have written back to everyone, but IF YOU HAVEN'T HAD AN EMAIL ACKOWLEDGEMENT PLEASE WRITE AGAIN. Unfortunately there have been some problems with out mail delivery system, and some important incoming messages have been lost recently. Things are in chaos at the moment because the Department of Computer Science at QMW is moving from one building to another (the postal address and phone numbers stay the same though). It seems that I overdid it in diverting people away from the earlier chapters to the later ones. There hasn't been much take-up on chapters 1 and 2. The second has been (re)written quite recently. If, like me, you believe that so-called "discrete math" is a mass of confused dogma and desparately in need of reform then chapter 2 will give you something to think about (I don't claim to have effected the reform). The web address for more information is http://www.dcs.qmw.ac.uk/~pt/book/index.html Paul Taylor Date: Fri, 22 May 1998 15:00:05 +0100 (BST) From: Paul Taylor Subject: categories: "Practical Foundations of Mathematics" Practical Foundations of Mathematics, ISBN 0-521-63107-6 To be published by Cambridge University Press, as number 59 in their series Cambridge Studies in Advanced Mathematics (which includes books by Peter Johnstone and by Jim Lambek and Phil Scott). Please see http://www.dcs.qmw.ac.uk/~pt/book/index.html for details. This is the LAST CALL FOR COMMENTS. The text is already in the hands of the copy editor for the second time. CUP hopes to have it published in time for the International Congress of Mathematicians in Berlin in August, which means I have to finish it by the end of May. I am aware that my policy of only giving away single chapters has annoyed people a bit, but it has been successful in its objective of getting attention for the whole book. (The most assiduous reader of "Proofs and Types" got to chapter 12 out of 15). I don't intend to distribute any more chapters now, though if I owe you a copy of the whole draft because you sent me comments on a chapter, please ask (tearing apart sections 1.1 and 1.2 does not count). If you have a copy of part of the book and have noticed a mis-conception, please SPEAK NOW OR FOREVER HOLD YOUR PEACE. There is really no point in telling me about missing commas in any but the most recent versions (ie 1998) as other readers, the copy editor and I have been through the text several times since I last distributed copies (in July 1997). When I am rid of the book itself, I intend to set up a web site as a repository for citations, discussion, answers to exercises and, inevitably, corrections. With the permission of the people concerned, I intend to publish some of the correspondence I have had about the book in this way, and there will be automatic facilities for readers to add further comments. Therefore any comments you have about the book which are too late for publication or which are not suitable for inclusion will not be wasted. I would like thank Pierre Ageron, Lars Birkedal, Luca Cattani, Michel Chaudron, Thierry Coquand, Robert Dawson, Luis Dominguez, Peter Dybjer, Susan Eisenbach, Fabio Gadducci, Gillian Hill, Martin Hyland, Samin Ishtiaq, Achim Jung, Stefan Kahrs, J\"urgen Koslowski, Steve Lack, Jim Lambek, Charles Matthews, Paddy Mccrudden, James Molony, Edmund Robinson, Pino Rosolini, Martin Sadler, Alan Sexton, Thomas Streicher, Charles Wells, Graham White, Andrew Wilson and Todd Wilson for taking the trouble to read parts of the draft and giving their detailed comments on it. (Please tell me if you think you should be on this list but aren't.) Paul Taylor Date: Thu, 18 Mar 1999 20:44:39 GMT From: Paul Taylor Subject: categories: "Practical Foundations of Mathematics" Practical Foundations of Mathematics Paul Taylor Department of Computer Science Queen Mary and Westfield College London E1 4NS http://www.dcs.qmw.ac.uk/~pt/book/ Cambridge Studies in Advanced Mathematics #59 (the series in which "Stone Spaces" by Johnstone and "Introduction to Higher Order Categorical Logic" by Lambek and Scott appeared.) ISBN: 0-521-63107-6 xii+576 pages List price: £50 or $80 I understand that the text and cover have now been printed, and are due to be bound on Monday 22 March in Cambridge, so I expect to see my own copy by the end of next week; orders should be dispatched after the Easter holiday. PLEASE SEE BELOW FOR THE BEST WAY TO ORDER YOUR COPY. The (not very informative) names of the chapters are: I First Order Reasoning VI Structural Recursion II Types and Induction VII Adjunctions III Posets and Lattices VIII Algebra with Dependent Types IV Cartesian Closed Categories IX The Quantifiers V Limits and Colimits The back cover "blurb" reads: Practical Foundations collects the methods of construction of the objects of twentieth century mathematics. Although it is mainly concerned with a framework essentially equivalent to intuitionistic ZF, the book looks forward to more subtle bases in categorical type theory and the machine representation of mathematics. Each idea is illustrated by wide-ranging examples, and followed critically along its natural path, transcending disciplinary boundaries between universal algebra, type theory, category theory, set theory, sheaf theory, topology and programming. The first three chapters will be essential reading for the design of courses in discrete mathematics and reasoning, especially for the ``box method'' of proof taught successfully to first year informatics students. Chapters IV, V and VII are an introduction to categorical logic. Between the formal languages translations are provided which are fluent, showing how to write vernacular proofs which are sound in formal logics. Chapter VI is a new approach to term algebras, induction and recursion, which have hitherto only been treated either naively or with set theory. The last two chapters prove in detail the equivalence of types and categories, in particular between generalised algebraic theories and categories with display maps. Students and teachers of computing, mathematics and philosophy will find this book both readable and of lasting value as a reference work. The web page currently just gives just the list of contents (down to the names of subsections), but when I have time to work on it I intend use it to publish many of the specific comments that people have made about the text (if those people are willing), and provide an interface for making further comments, and, of course, corrections. CUP has indicated that they have no objection to my publishing the entire text on the web in any form short of a printable DVI or PS file; when I have found a translator that actually works on my text, I intend to make an HTML version, obviously without most of the mathematical formulae, to feed to the web crawlers. HOW BEST TO ORDER YOUR COPY This depends on whether you would like to make a large donation to (a) your bookstore's profits: just quote the ISBN to them; (b) CUP's profits: fill in their web order form (no discount, by policy, and you pay cost of postage); (c) the UK Inland Revenue: wait until April 6 before you do anything; (d) the author, who has committed career suicide by writing this book at all. The special deal that I have negotiated is this. CUP is ADAMANT that it is contrary to their policy to give discounts for direct orders, even though the Web is now clearly the best way of ordering research-level books. However, by personal arrangement with my editor and the marketing manager, if you email, fax or phone the marketing manager, Richard Knott, email: rknott@cup.cam.ac.uk tel: +44 1223 325 916 fax: +44 1223 315 052, with your address and credit card number, mentioning that you saw this message from me, you get the book at list price INCLUSIVE of overland postage (normally £2.50), and I get some commission. If you want airmail delivery, there is an extra £2.50 charge. If you are not sure whether you actually want to buy the book yet, but you think you might (or might be teaching a course based on it) please email Richard Knott and say so, as soon as possible. If I get evidence of respectable sales prospects then I might persuade them to pay me an advance on royalties THIS MONTH - in the tax year during which I was unemployed for five months - instead of having a lump sum in May 2000 taxed at 40%. Please, this is important if you think that academic authors deserve some reward for the labour and demoralisation of eight years writing a book. £50 is pretty good value for a research book of this size. A recently announced book on similar material, published by the Dutch company Elsevier (North-Holland) costs TWICE the price (for 1/3 more pages). CUP, being part of Cambridge University, has no shareholders and counts as a charity for tax purposes, and there is no VAT on books in Britain. Even so, other recent books of same size in the same series as mine retail at £65. I kept the price of mine down by doing the whole of the typographical work myself (of course), and by NOT claiming the £2350 that I could have got for providing lower quality camera-ready hard copy instead of PostScript. Paul PS Unfortunately, despite my best efforts, I was not able to negotiate a reduction in the Bank of England's interest rates, and therefore in the present absurdly high Sterling exchange rate. Sorry. I will try to do better next time. CUP's postal address is Cambridge University Press, The Edinburgh Building, Shaftesbury Road, Cambridge, CB2 2RU, UK. Date: Sun, 21 Mar 1999 20:07:56 GMT From: Paul Taylor Subject: book: "Practical Foundations of Mathematics" Announcing... Practical Foundations of Mathematics Paul Taylor Department of Computer Science Queen Mary and Westfield College London E1 4NS http://www.dcs.qmw.ac.uk/~pt/book/ Cambridge University Press Cambridge Studies in Advanced Mathematics #59 (the series with a grey cover and a diagonal coloured stripe) ISBN: 0-521-63107-6 xii+572 pages List price: £50 or $80 Being bound, Monday 22 March in Cambridge (UK) PLEASE SEE BELOW FOR THE BEST WAY TO ORDER YOUR COPY. The (not very informative) names of the chapters are: I First Order Reasoning VI Structural Recursion II Types and Induction VII Adjunctions III Posets and Lattices VIII Algebra with Dependent Types IV Cartesian Closed Categories IX The Quantifiers V Limits and Colimits The back cover "blurb" reads: Practical Foundations collects the methods of construction of the objects of twentieth century mathematics. Although it is mainly concerned with a framework essentially equivalent to intuitionistic ZF, the book looks forward to more subtle bases in categorical type theory and the machine representation of mathematics. Each idea is illustrated by wide-ranging examples, and followed critically along its natural path, transcending disciplinary boundaries between universal algebra, type theory, category theory, set theory, sheaf theory, topology and programming. The first three chapters will be essential reading for the design of courses in discrete mathematics and reasoning, especially for the ``box method'' of proof taught successfully to first year informatics students. Chapters IV, V and VII are an introduction to categorical logic. Between the formal languages translations are provided which are fluent, showing how to write vernacular proofs which are sound in formal logics. Chapter VI is a new approach to term algebras, induction and recursion, which have hitherto only been treated either naively or with set theory. The last two chapters prove in detail the equivalence of types and categories, in particular between generalised algebraic theories and categories with display maps. Students and teachers of computing, mathematics and philosophy will find this book both readable and of lasting value as a reference work. The web page currently just gives just the list of contents (down to the names of subsections), but when I have time to work on it I intend use it to publish many of the specific comments that people have made about the text (if those people are willing), and provide an interface for making further comments, and, of course, corrections. CUP has indicated that they have no objection to my publishing the entire text on the web in any form short of a printable DVI or PS file; when I have found a translator that actually works on my text, I intend to make an HTML version, obviously without most of the mathematical formulae, to feed to the web crawlers. HOW BEST TO ORDER YOUR COPY This depends on whether you would like to make a large donation to (a) your bookstore's profits: just quote the ISBN to them; (b) CUP's profits: fill in their web order form (no discount, by policy, and you pay cost of postage); (c) the UK Inland Revenue: wait until April 6 before you do anything; (d) the author, who has committed career suicide by writing this book at all. The special deal that I have negotiated is this. CUP is ADAMANT that it is contrary to their policy to give discounts for direct orders, even though the Web is now clearly the best way of ordering research-level books. However, by personal arrangement with my editor and the science/technology marketing person, if you contact Richard Knott, email: rknott@cup.cam.ac.uk fax: +44 1223 315 052 tel: +44 1223 325 916 (by other methods are preferable) snail: Cambridge University Press, The Edinburgh Building, Shaftesbury Road, Cambridge, CB2 2RU, UK with your address and credit card number, mentioning that you saw this message from me, you get the book at list price INCLUSIVE of overland postage (normally £2.50), and I get some commission. If you want airmail delivery, there is an extra £2.50 charge. (The basis on which I get commission is that I am using my contacts, ie this message, to do part of Richard Knott's job for him.) If you are not sure whether you actually want to buy the book yet, but you think you might (or might be teaching a course based on it) please email Richard Knott and say so, as soon as possible. If I get evidence of respectable sales prospects then I might persuade them to pay me an advance on royalties THIS MONTH - in the tax year during which I was unemployed for five months - instead of having a lump sum in May 2000 taxed at 40%. Please, this is important if you think that academic authors deserve some reward for the labour and demoralisation of eight years writing a book. £50 is pretty good value for a research book of this size. A recently announced book on similar material, published by the Dutch company Elsevier (North-Holland) costs TWICE the price (for 1/3 more pages). CUP, being part of Cambridge University, has no shareholders and counts as a charity for tax purposes, and there is no VAT on books in Britain. Even so, other recent books of same size in the same series as mine retail at £65. I kept the price of mine down by doing the whole of the typographical work myself (of course), and by NOT claiming the £2350 that I could have got for providing lower quality camera-ready hard copy instead of PostScript. PS Unfortunately, despite my best efforts, I was not able to negotiate a reduction in the Bank of England's interest rates, and therefore in the present absurdly high Sterling exchange rate. Sorry. I will try to do better next time. Paul Taylor --- real email address (without "2") Please do not send any email to pt2@... which is a special account created to collect mail errors, or categories@... which is a defunct local redistribution list that I've borrowed temporarily to dispatch this message and will then immediately disable (the real category theory bulletin board is ).