Subject: categories: errata to "Practical Foundations"

From: Paul Taylor <[email-masked]>
Date: Sat, 19 Aug 2000 16:04:12 +0100

ERRATA TO    "PRACTICAL FOUNDATIONS OF MATHEMATICS"

I would like to thank   David Benson,  Peter Johnstone,  Thomas Streicher
and  Krzysztof Worytkiewicz  for their comments in response to my request
for corrections.  If you know of any other mistakes, please tell me ASAP.

First, I apologise to Heinrich Kleisli, Dito Pataraia, Maria Cristina
Pedicchio, Dietmar Schumacher and V. Z\"oberlein for my mistakes in
their names on pages 179, 403, 533, 540, 563, 566 and 572.

Only one actual falsity has come to my attention:  exactly a year after
I got the first copy of the book, Thomas sent me a simple counterexample
to the claim that fibrations preserve pullbacks (Exercise 9.4, page 523).

I am very pleased at how few errors have shown up in 17 months, and how
trivial they are.   This is a tribute to the care that nearly 40 people
took in reading individual chapters of the book.  Though I am sure that
this policy of only sending out single chapters irritated the people in
question, it did prove to be a very successful way of ensuring that the
entire book got careful and reasonably even attention. In contrast, the
most assiduous reader of "Proofs and Types"  only got two thirds of the
way through the book, starting from the beginning.

You may like to read Peter Johnstone's review for the Zentralblatt at
   http://www.dcs.qmw.ac.uk/~pt/Practical_Foundations/Johnstone-review.html
(it's on my web site because it's unreadable on the Zentralblatt site).

There is an 18 page summary of the contents of the book at
   http://www.dcs.qmw.ac.uk/~pt/Practical_Foundations/summary.dvi
   http://www.dcs.qmw.ac.uk/~pt/Practical_Foundations/html/summary.html
The DVI version is intended for you to print, the HTML one for linking
into the full text of the narrative that's also on the web.

The bibliography is available as a BibTeX file at
   http://www.dcs.qmw.ac.uk/~pt/Practical_Foundations/prafm-ref.bib

I understand that 1000 copies were printed in March 1999, of which 825
had been sold when I asked last week, and 400 new ones are to be printed.
For over seven years' work, I have had about 3000 pounds in royalties
and no permanent job.

SIGNIFICANTLY WRONG SYMBOLS AND WORDS

p. 37, Lemma 1.6.3, proof box, line 6:
should be \exists y.\gamma\land\phi[y] in the left-hand box.

p. 144, intro to Section 3.5, and p. 176, Exercise 3.19:
the sum of posets or dcpos (not domains).
  
p. 275, final paragraph of Definition 5.5.1: if c then ... (not a).
  
p. 285 Corollary 5.6.12: v(y)=x_1, not u_y=x_1.

p. 290, diagram for Lemma 5.7.6(e):
(German) f;m and z;n instead of f;n and z;m.

p. 362, Exercise 6.23:
T\Theta instead of T(\Gamma\times\Theta) at the top right of the diagram.

p. 397, introduction to Section 7.5: \mu = U\epsilon F.

p. 415, Notation 7.7.3(b)  Q_X: H_X \to U `X'.

p. 519, Proposition 9.6.13 [c=>a]: The infinitary version of
Example 2.1.7, rather than of its converse {Exercise 2.14).

The full list of actual changes (including broken sentences and places where
inserting a couple of extra words could improve understandability) is at
   http://www.dcs.qmw.ac.uk/~pt/Practical_Foundations/errata.html

REMARKS ON OTHER POINTS THAT I FEEL I UNDERSTAND BETTER SINCE PUBLICATION

The Substitution Lemma (1.1.5, p. 7) correctly forbids x to be free in a,
because the substitution  [a/x]^*u  is meant to result in a term that
doesn't involve x. See Definition 4.3.11(b) for why.  Arguably, contexts
should be emphasised from the start, especially as, in this book, they turn
into the objects of the classifying category.  That the proof of the
Substitution Lemma tolerates  x  being free in  a  entirely misses the
point,  and merely illustrates the tyranny of notation over concepts

In his review, Peter Johnstone teased me for Exercise 1.1 (Bo Peep's theorem).
To add fuel to his fire, I now think that the natural proof of this -
the very earliest theorem in mathematics - is essentially the argument
needed for the Schr\"oder-Bernstein theorem.  It would be nice to be able
to get an anthropologist to understand that this *is* a significant theorem,
and to try to find out at what stage in the development of human cultureS
it was learned.

p. 358, Remark 6.7.14: It is probably true in the concrete case of
ordinals in Pos and Set that a sh-coalgebra is well founded in the
sense of Definition 6.3.2 iff  <  is a well founded relation
(Definition 2.5.3).  Inability to formulate the abstract result for
ordinals in categories between which there is an adjunction  F -| U
is the reason why I have not finished [Tay96b].

p. 502, Example 9.4.11(d): The closed point of the Sierpi\'nski space
does classify closed subsets intuitionistically.   Any point of this
space can be expressed as the join of a directed diagram taking only
\bot and \top as values, whilst (the dual of) the equation in Exercise
9.57 characterises support classifiers [Tay98].

Section 9.4: Beware that, whilst my approach to the Beck-Chevalley
condition does ensure that pullbacks of  >---|>-maps  are  >---|>-maps,
such pullbacks do not always exist in the category of locally compact spaces.

Paul