Andrej Bauer asked about the INTERNAL LOGIC OF LEX CATEGORIES. He gave a sketch of such a logic, based primarily on EQUALITY. Another conspicuous feature is the SYMMETRY in the notions of equality, conjunction, product and pullback. The reason for being interested in such a logic is presumably in order to give interpretations of "generalised", "dependent-type" or "essentially" algebraic theories. The theory of categories is the leading example of this, the TYPE Hom(x,y) being dependent on the TERM-variables x and y. I would argue that lex categories are the WRONG structure in which to interpret such theories. SEMANTICALLY, there are lots of interesting categories (of domains, of locally compact spaces, of differentiable manifolds, and so on) that don't have all finite limits, but in which one would nevertheless like to interpret such theories. What, for example, is a locally compact topological groupoid? SYNTACTICALLY, equations conditional on equations are not how we think about, for example, composition in categories. When we are about to form "f;g", we already know that the target of f is the same object as the source of g - it is not an accidental situation whose validity we have to test "on the fly". (This point was made, using Kant's synthetic/analytic distinction, by John Cartmell in his treatment of generalised algebraic theories in JPAA in 1986.) Mathematicians have, traditionally, not bothered about such issues - "either the objects are equal or they're not" - but in a computational setting, it becomes significant if this equality needs to be tested "at run time". Proof theory also distinguished between INTENSIONAL and EXTENSIONAL equality. Generalised algebraic theories come first, equality is an add-on. In particular, we need to give account of the more basic syntactic notion of SUBSTITUTION. This is interpreted by pullback, but is by no means symmetric between the two legs: one is the term containing the free variable, the other the term to be substituted. On the semantic side, pullback often encodes INVERSE IMAGE, which is also asymmetrical. For example, in topology we use inverse images of OPEN subspaces and maps along ARBITRARY continuous functions. It was to capture this situation (specifically, in categories of domains) that I introduced CATEGORIES WITH DISPLAY MAPS in my 1987 PhD thesis (and earlier in CTCS1, LNCS 240). A class of display maps is simply one that is closed under pullback along any map in the category. I use an open-triangle arrowhead for such maps. Syntactically, a display map is a map between contexts that simply omits one (the last) typed variable: Gamma, z:Z ----|> Gamma This corresponds to WEAKENING in type theory. An arbitrary map Delta = [y1:Y1, ..., ym:Ym] ----> Gamma = [x1:X1, ..., xn:Xn] in this category assigns a term ai:Xi, possibly involving the ys, for each position in the target context. Pullback of the display map along this map substitutes these terms for the xs in the type Z, which may have depended on these variables. Terms of type Z in context Gamma are splittings of the display; these undergo substitution in the same way when we pull the splittings back along Delta->Gamma. You may think that, given a highly dependent system of types, this category (the CLASSIFYING CATEGORY or CATEGORY OF CONTEXTS AND SUBSTITUTIONS) would be complicated to construct. Indeed it is, if you approach it in the wrong way, as a huge structural recursion. But this is because, as functional programmers know very well, recursion does not interact well with associativity. There is, in fact, an EASY AND UNIFORM CONSTRUCTION of the category from ANY TYPE THEORY that has all of the usual structural rules, in particular weakening (so this doesn't apply to linear logic). However, we obtain the category via an (elementary) SKETCH: - the objects are contexts, - the morphisms are GENERATED from two classes: - display maps (weakening by a typed variable) and - their splittings (cut with a typed term). - the equations are (those of the theory) plus five more, of which the well known SUBSTITUTION LEMMA is the most complicated. The place to look for the details of this is not my thesis, but CHAPTER VIII of my book, "Practical Foundations of Mathematics" Cambridge University Press, 1999 http://www.dcs.qmul.ac.uk/~pt/book/html/c8.html As I said, I introduced display maps in my thesis for domain theory, and in particular to discuss dependent products (polymorphism). The point was that NOT ALL SUCH PRODUCTS EXIST, as they do in Set, for which Lawvere had introduced the notion of HYPERDOCTRINE. As I was interested in constructing dependent products in semantic categories, it was important to seek ways of simplifying the calculations as much as possible. Ultimately, I found that only the special case of so-called PARTIAL PRODUCTS was needed. This reduction is in Section 9.4 of the book. The rest of Chapter IX deals with other aspects of type theories. Paul Taylor 17-Dec-2002 19:04:31 -0400,3589;000000000001-00000000