I agree with Jean Benabou, Fred Linton and Vaughan Pratt that the definition of a locally cartesian closed category should NOT require a terminal object. I expressed this view in a footnote on page 499 of "Practical Foundations of Mathematics", with a justification similar to Vaughan's. The simplest formulation is that an LCCC is a category every slice of which is a CCC. In particular, every slice has binary products, which are pullbacks in the whole category. Objects of an LCCC and the slices that they define correspond to objects of a base category and the fibres over them in a fibred or indexed formulation of logic, and to contexts in a syntactical one. Contexts are collections of hypotheses. The terminal object or empty context is the one with no hypotheses at all. However, as the 18th century logician Johann Lambert remarked, ``no two concepts are so completely dissimilar that they do not have a common part''. If "naturally occurring" LCCCs usually have terminal objects, I suggest that that may be because they are already slices of some more general picture. For more or less the same reason, we never actually concatenate two contexts, but build them up one hypothesis at a time. So I would say that, whilst an LCCC has pullbacks, it need not have binary products. (My footnote refers to "other authors" who said that LCCCs should have binary products; I think I may have had Thomas Streicher in mind, but I don't recall what he may have said or in what paper.) I confess that I'm a bit surprised to find that the consensus agrees with me, so to set matters straight I should also point out that my argument applies equally to elementary toposes and other familiar structures of categorical logic. ---- While we're playing around with the structures of categorical logic, let me try another related question. Any topos is a CCC with an internal Heyting algebra. [WARNING TO STUDENTS: whilst this statement is true, it's NOT (equivalent to) the correct definition.] I am sorry to say that I have seen papers emanating from respectable universities in which the authors have appeared to believe that this is the definition. (One of the papers that I have in mind cites many eminent categorists, who may perhaps have an opinion about having their names appear alongside a lot of complete nonsense.) But I wonder whether anyone has taken this idea seriously, and investigated how much logic such a category would admit? The version of this question that particularly interests me is this: Suppose that the category has all FINITE LIMITS (terminal object, finite products and equalisers) and POWERS Sigma^X of an internal DISTRIBUTIVE LATTICE (Sigma, top, bot, meet, join). Maybe there is also a natural numbers object N and joins Sigma^N->Sigma with the Frobenius law. (I would also like this to obey the monadic and Phoa principles of ASD, but I'm not going to spell them out here.) Maps X->Sigma give rise to a "geometric logic" of "open" subspaces. Then the order relation between maps X->Sigma^Y leads to a richer logic of "general" subspaces, with => and forall_Y. A logical formula of the more general form consists of geometric sub-formulae joined together with => and forall, to which we might add the other first order connectives as "syntactic sugar", defined in the usual classical way. If a geometric sub-formula is immediately enclosed in forall_K or exists_N, where K happens to be compact or N overt, then this a priori more general quantifier may be considered to be part of the geometric sub-formula. Does this idea ring any bells? Paul Taylor