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