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 <pt@dcs.qmw.ac.uk>

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 <pt@dcs.qmw.ac.uk>


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 <pt@dcs.qmw.ac.uk>

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 <pt@dcs.qmw.ac.uk>


Date: Fri, 22 May 1998 15:00:05 +0100 (BST)
From: Paul Taylor <pt@dcs.qmw.ac.uk>
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 <pt@dcs.qmw.ac.uk>
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 <pt2@dcs.qmw.ac.uk>
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 <pt@dcs.qmw.ac.uk>  (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 <categories@mta.ca>).