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

- p. x before Acknowledgements:
topics in
*the mechanics of*symbolic logic using the methods*of*category theory. - p. xi: Ruth Horner died the very week that the book went to press, and Doris Wilson died during the following year.

- p. 1, para 2:
*characteristic*instead of*remarkable*- this seems to be a pretty good definition of the mathematical sciences. - p. 4, Remark 1.1.1:
The simplest operation on trees
is substitution of
*another*term for a variable. A copy of the expression-tree*for*the new term is made for*each*occurrence of the variable, and attached to the tree in its place. If there*are*many occurrences, the*new*term and its own variables*are*proliferated, but if there*are*none the new term*disappears*. - p. 7, Lemma 1.1.5:
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. - p. 9, Definition 1.1.9:
In fact ... In this book we make (not make make) no systematic distinction.
- p. 17, Definition 1.2.10(a)
(broken sentence structure):
by at most one thing,
*so that any two (") solutions are equal*(*cf*. Example 1.8.2): - p. 34, Remark 1.5.9:
so the sign
*(positive or negative)*of the influence of f depends on whether it lies behind an odd or even number of implications. - p. 37, Lemma 1.6.3,
proof box, line 6 (
**significantly wrong symbol**): should be $*y*.g\landf[*y*] in the left-hand box; for clarity, I have put (g\landf)Ú¼ and ¼Ú(g\landy) in the right-hand box too. - p. 50, Remark 1.7.9(b):
f[
*x*] without an arrow under the*x*. - p. 60, Exercise 1.1:
She found a stick or a pebble for
*(to ``name'')*each individual sheep, and moved*it*from a pile outside the pen to another inside. Any one object*(not necessarily the sheep's own ``name'')*. [*Hint: cf**Exercise 3.63*.] (I now think that the Schröder-Bernstein theorem is the proof of this, which will of course add fuel to Peter Johnstone's fire.) - pp 60-1, Exercise 1.5:
Show how to express a Turing machine as a
*system of reduction rules*.

- p.93, before Remark 2.4.10:
The failure of the disjunction property
*seems to mean that classical logic*has no constructive interpretation.

- p. 128, Warning 3.1.4:
Any irreflexive relation < [insert "("
*x*.*x*\not <*x*)"] can in fact be recovered from ( < )È( = ) - p. 128: Example 3.1.6(c):
The composite of two monotone functions
*(or of two antitone ones)*is*again*monotone. - p. 132: Example 3.2.5(h)
(
**misleading remark**):*Example 6.6.3(f)**shows that Á Ì {^,T} can only be regarded as finite if it's a complemented subset.* - p. 133: mark on plate in Example 3.2.8,
near the right.
- p. 143, Definition 3.4.10
(
**misleading remark**): The type 2/W of truth values is playing a topological role here, in which the point T is open and ^ is closed.*As such, 2/W is called the Sierpinski space and will be written*. (The remark about being ``intermediate'' is misleading, as 2/W is indeed the set of points of the Sierpinski space intuitionistically.)*S*. As with**R**, in this book we shall avoid questions that rely on the intuitionistic nature of this space (see the footnote on page 502) - p. 144, intro to Section 3.5
(
**significantly wrong word**): the sum of posets or*dcpos*. - p. 160, second paragraph of
Remark 3.7.12:
Cf [Con76, p. 66]
(This was essentially the point of
John Conway's ``Mathematicians' Liberation Movement''.)
- p. 162: "Modal logic has medieval and even ancient roots" belongs
*after*Definition 3.8.2. - p. 162, before Example 3.8.3(b'):
but
*the second*, partial correctness. - p. 165: mark on plate in middle of
Theorem 3.8.11(a).
- p. 176, Exercise 3.19
(
**significantly wrong word**): posets or*dcpos*. - p. 179, Exercise 3.45:
*Dito*Pataraia.

- p. 238, after Proposition 4.8.3
(
**significantly wrong word**):*naturality*, not*normality*. - p. 243, Definition 4.8.15(c)
(
**significantly wrong word**): the right*end*of the first cell is the left*end*of the second.

- p. 275, penultimate paragraph of
Definition 5.5.1:
The bottom row
*f the rectangle*... products.*Then*... - final paragraph (
**significantly wrong symbol**):**if***c***then** - p. 285 Corollary 5.6.12
(
**significantly wrong symbol**):*v*(*y*) =*x*_{1}. - p. 288, Lemma 5.7.3:
use
*W*instead of*K*, for just this lemma, as it's about coequalisers in general rather than kernels. Conversely,*given equal*, apply orthogonality.*W*\rightrightarrows*B*® Q - p. 290, diagram for Lemma 5.7.6(e)
(
**significantly wrong symbol**): (German)*f*;*m*and*z*;*n*instead of*f*;*n*and*z*;*m*. - p. 295, Remark 5.8.4(e):
The lifting property is not unique, but there's no room to insert this.

- p. 342, Remark 6.5.6:
[Knu68, vol. 1, pp. 353-5]
explains how to store the equivalence relation.
- p. 346, Example 6.6.3(f):
a subset of a finite set is finite iff it is complemented
*cf. Example 3.2.5(h)*. - p. 346, after Remark 6.6.4:
the ambiguity in the usage of
*the word ``law''*mentioned in Definition 1.2.2. - p. 350, Corollary 6.6.12:
{^,T} is a
*join*-semilattice; the unique*join*-homomorphism taking all singletons to T maps everything else there except Æ. - 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 \prec is a well founded relation (Definition 2.5.3). Inability to formulate the abstract result for ordinals in*A*and*C*where there is an adjunction*F*\dashv*U*is the reason why I have not finished [Tay96b]. - p. 362, Exercise 6.23
(
**significantly wrong symbol**):*T*Q instead of*T*(G×Q) at the top right of the diagram.

- p. 380, proof of
Theorem 7.2.2[
*b*Þ*c*]: Putting*B*=*FX*. - p. 397, introduction to Section 7.5
(
**significantly wrong symbol**):m =

*U*·e·*F*. - p. 403, Remark 7.5.12: V. Zöberlein.
- p. 415, Notation 7.7.3(b)
(
**significantly wrong symbol**):*Q*_{X}:*H*_{X}®*U*`*X*¢.

- p. 436, diagram for Example 8.1.12:
the arrows marked [^(
*f*)][^(*x*)] and [^(*g*)][^(*z*)] should have double arrowheads, but this hasn't been changed.

- p. 472 Notation 9.1.3:
mark on plate near ``Note that nothing we did in Chapter VIII''.
- p. 480, Example 9.2.5,
last paragraph: I find this example very confusing as the
main
*one*used to demonstrate. - p. 487, Remark 9.3.1:
several marks on the plate.
- p. 489, Remark 9.3.3,
last line of the dotted proof box
(
**significantly wrong symbol**): [*a*/*x*,*b*/*y*]^{*}*f*:q. - p. 491, Definition 9.3.6:
the slanted pullback symbol has been made parallel with the relevant map.
- p. 491, Corollary 9.3.9:
Our Frobenius law follows
*as*a corollary. - p. 502, Example 9.4.11(d)
(
**misleading remark**):*Although ^ Î 2/W doesn't classify subsets in*Exercise 9.57*Set*intuitionistically, in*Sp*the closed point of the Sierpinski space does classify closed subsets. Any point of*S*can be expressed as the join of a directed diagram taking only ^ and T as values, whilst (the dual of) the equation in*characterises support classifiers*[Tay98]. - pp 505, after Corollary 9.4.16
(
**misleading treatment**): Beware that, whilst our approach to the Beck-Chevalley condition does ensure that pullbacks of`>-|>`-maps are again`>-|>`-maps, such pullbacks need not always*exist*in the category of locally compact spaces. - p. 506, Section 9.5:
In fact the formal rules also suggest that we should view comprehension
*as forming types or contexts from contexts and not types*. - p. 519,
Proposition 9.6.13[cÞ]:
*The infinitary version of**Example 2.1.7*(rather than of its converse Exercise 2.14). - p. 523, Exercise 9.4
(
**the one and only falsity**): Thomas Streicher sent me a simple counterexample to the claim that fibrations preserve pullbacks. I have replaced the exercise with*Let**C*and*S*be categories with pullbacks and*P*:*C*®*S*a functor that preserves them. Suppose that*P*\dashv*T*with*P*·*T*=*id*_{S}. Show that*P*is a fibration. Find a fibration of posets that preserves neither \land nor T.

- [BHPRR66]
Essays
*on*the foundations of mathematics.