Paul Taylor gave an example of a unification that he says refuted something he said in Manchester. Unfortunately, it also refutes Theorem 8.7.4 of CTCS. He wrote:

Here is an example of computer science interest, and a counterexample to what I claimed (privately) at the recent Manchester PSSL. David Rydeheard's book discusses unification (as used in logic and functional programming) as a coequaliser in the Kleisli category for the monad for an algebraic theory with no equations. A very simple example shows that this is *not* the coequaliser in the category of algebras. Take one unary operation f and two variables x,y. Then as a unification problem the equation f(x)=f(y) implies x=y, but the coequaliser as an algebra is essentially "N with two zeroes".

I ran this example through our proof and found the mistake. On l. 2 of 226 we refer to exercise 3, which says that a map between free algebras for a free theory is either epimorphic or factors through a proper subset of any free generating set. The problem is solved and from the solution, although not from the statement, it is clear that this is true only in the category of free algebras. In fact PT's example gives a trivial counter-example to that too. The map from F1 to F1 that applies f to the generator is epi in the category of free algebras, but not in the category of all algebras; there are two maps from F1 to "N with two zeroes" that agree on the image. Thus the conclusion, that there is a coequalizer, is valid, but only for the category of free algebras. It is not the coequalizer in the algebra category. The statement has to be reworded, but so does the proof because it has to be reworded as a construction of a coequalizer in the Kleisli category. The details are quite easy and we leave it to the reader. Michael ===================================================================