John Mitchell wrote
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.
You might have a look at my chapter on "Basic Category Theory" in the "Handbook of Logic in Computer Science (Abramsky, Gabbay, maibaum eds.), OUP, 92. There I follow your program to use an explicit list of free variables which gives a reasonable account how composition in categories relates to substitution on free variables (as opposed to application where bound variables are substituted) (mainly in sections 1,2, 8).
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?
in principle not, but it seems that UAs use sorts for the syntactic entities and types for the semantic ones. In a way, type theory talks about both levels. Axel Poigne ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++