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 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.
Such as cartesian closed categories, for instance. I would like to take the opportunity to point to my paper "Life without the terminal type" in CSL 2001, where I prove that every "almost" cartesian category, i.e. one without a terminal object, extends uniquely to a cartesian closed category with terminal object. There is also a similar result for toposes; the wording is not quite as straightforward as for cartesian closed categories, as one has to formulate (say) the definition of a subobject classifier without reference to a global element True. I recall having thought about locally cartesian closed categories as well, but I do not think I really got anywhere (and actually I just see there's a remark in the paper that says as much). Lutz Schröder -- ------------------------------------------------------------------ PD Dr. Lutz Schröder office @ Universität Bremen: Senior Researcher Cartesium 2.051 Safe and Secure Cognitive Systems Enrique-Schmidt-Str. 5 DFKI-Lab Bremen FB3 Mathematik - Informatik Robert-Hooke-Str. 5 Universität Bremen D-28359 Bremen P.O. Box 330 440 D-28334 Bremen phone: (+49) 421-218-64216 Fax: (+49) 421-218-9864216 mail: Lutz.Schroeder@dfki,de www.dfki.de/sks/staff/lschrode ------------------------------------------------------------------ ------------------------------------------------------------- Deutsches Forschungszentrum für Künstliche Intelligenz GmbH Firmensitz: Trippstadter Strasse 122, D-67663 Kaiserslautern Geschäftsführung: Prof. Dr. Dr. h.c. mult. Wolfgang Wahlster (Vorsitzender) Dr. Walter Olthoff Vorsitzender des Aufsichtsrats: Prof. Dr. h.c. Hans A. Aukes Amtsgericht Kaiserslautern, HRB 2313 -------------------------------------------------------------