Reply to a question by J"urgen Koslowski (from 26 Oct 92). In logic and type theory, variables are there for human convenience. They are just pointers, which are given names. Such names are often used `locally' (i.e. in a specific term or formula) with an implicit convention that there are no `global' name clashes. Category theory provides a variable-free formalism for logics and type theories. One uses projections instead of variables. Things become more precise, but less readable. In constructing categories from syntax (as I did in Example 3.2 of my Durham 1991 paper in LMS 177, to which J"urgen refers), one can either use a very precise syntax (e.g. with de Bruijn indices) or be very sloppy and hope the reader is willing to understand things in the appropriate way. Clearly I have chosen the latter approach. Below is a syntax for variables and contexts in simply typed lambda calculus, which solves the problems mentioned by J"urgen. It is not the syntax which is used in practice, but it is still readable. I'll use semi-LaTeX and write the letters `s' and `t' for types \sigma and \tau and `G' and `D' for contexts \Gamma and \Delta. Fix an infinite set Var = {v_1, v_2, v_3,...} of variables. A context is defined to be a finite sequence of types written as G = v_1:s_1, ..., v_n:s_n where by convention one counts the variables starting from 1. Assume another context D = v_1:t_1, ..., v_m:t_m then the concatenation G,D is defined to be G,D = v_1:s_1, ..., v_n:s_n, v_n+1:t_1, ..., v_n+m:t_m In this way no variable clashes occur (and hence no overwriting). The projections are the (equivalence classes of the) sequences (v_1,...,v_n) : G,D --> G (v_n+1,...,v_n+m) : G,D --> D This makes G,D the cartesian product of contexts G and D in the base category of contexts in Example 3.2 in loc. cit. I assume J"urgen now wants to know the rules for handling such `canonical contexts'. Here they are. PROJECTION ---------------- v_1:s |- v_1:s WEAKENING G |- M:t ---------------- G,v_n:s |- M:t (where G is supposed to be of length n-1) CONTRACTION G,v_n:s,v_n+1:s |- M:t --------------------------- G,v_n:s |- M[v_n/v_n+1]:t EXCHANGE G,v_i:s_i,v_i+1:s_i+1,D |- M:t ----------------------------------------------------- G,v_i:s_i+1,v_i+1:s_i,D |- M[v_i/v_i+1,v_i+1/v_i]:t Using such a precise syntax the problem raised by J"urgen can be solved. I did not put it in the paper because I thought it would distract too much. Bart Jacobs. Address since Aug.1, 1992: Mathematical Institute, RUU P.O.Box 80.010 3508 TA Utrecht The Netherlands Email: bjacobs@math.ruu.nl ==============================================================================