Thorsten Altenkirch says

Named variables are a complete redherring.

Named variables are the way that human mathematicians have been notating their work for centuries, and human programmers prefer them too. Even categorists give up \pi_1 and \pi_2 shortly after introducing the universal property of products! Thorsten also mentioned alpha conversion. There's an important distinction to be made with alpha conversion which corresponds to that between free (open) and bound (closed) variables. The closed term $\lambda x.x$ is to all intents and purposes the same as $\lambda y.y$ (and with de Bruijn indices *is* the same) but the open terms are quite different. My personal way of formulating this construction is as follows: * the objects are (finite) sets of distinct variable names together with their types, ie contexts; [x1:x1,x2:X2,...,xn:Xn] changing the names gives a different object * the morphisms are substitutions: [y1:=u1,y2:=u2,...,ym:=um] [x1:X1,x2:X2,...xn:Xn] ---------------------------> [y1:Y1,...,ym:Ym] where there's one "assignment" for each variable in the target context and the terms have their variables amongst those in the source. * composition is given right to left by the notationally simple rule [z:=v(y)] o [y:=u(x)] = [z:=v[y:=u]] I missed something out in the definition of morphism: I define *two* categories, one ("raw terms") consisting of closed-alpha equivalence classes, the other ("terms") being its quotient by beta/eta/etc equivalence. Similar constructions may be done for languages other than the simply typed lambda calculus. In fact lambda abstraction is not relevant to the issue. Now we may ask some elementary categorical questions: What are the isomorphisms in the category of *raw* terms? They are exactly the open alpha equivalences. In particular a context with two variables of the same type has a non-trivial automorphism. What do we get from concatenating two contexts which share no variable name? Assuming that the language admits individual variables as terms, allowing omission (weakening) and repetition (contraction), we obtain a product diagram. How can we form the product of contexts which do share variables, in particular the square of a context? We replace one or both by isomorphic copies (along open-alpha equivalences, ie renaming variables) and take the product of those. It seems to me that for any purpose other than the machine implementation of a compiler it is notationally better *not* to adopt a convention for consistently renaming variables in order to provide a canonical product in all cases. The product always *exists*, as I have shown (so long as we have an inexhaustible supply of new variable names), and there is a canonical choice of it, albeit involving an exception. If you're worried about the constructivity of the exception, remember that the variable names must have been chosen from amongst a decidable population, because I began by saying that they were distinct in each context (object). Paul Taylor ==============================================================================