I'm glad to see this discussion. In the book that I am (still) writing, I went to some length to do all the universal algebra with explicit lists of variables. At times, I have wondered whether this was syntactic overkill. However, it makes for clean completeness theorems and existence of initial algebras. In addition, it meshes well with later chapters on typed lambda calculi, where contexts (lists of variables and their types) are needed. One minor question, while I am thinking of it. I used "sort" in the chapter on algebra, and "type" in the chapters on lambda calculi, etc. What do the UA-literate think about using "type" uniformly throughout? Would it be offensive to simplify terminology this way? BTW, there is not much math in the chapter on UA, just soundness, completeness, homomorphisms, initiality, and a number of CS examples (stacks, queues, trees, ...), ending with a brief overview of rewrite systems. John Mitchell ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++