Hi Emily and everybody if something should be called 'locally cartesian closed category', I think we should at least read the words and ponder what they say. Those four words do not imply anything about a terminal object (just as they do not suggest the existence of finite sums). I am surprised this is not the end of the discussion, but we are a very social community :-) It seems that the only argument in favour of sneaking in the extra condition of having a terminal object is that the phrase has been used in that way in the past, even in a very authoritative source like the Elephant. I don't think that argument should be given much weight. Peter already admitted it was laziness. He said that there was a terminal object in all examples known to him -- except one example which he decided to exclude, cold-bloodedly :-) I don't mean to criticise the Elephant -- let alone its author! It is fine to repurpose terminology a bit, without being dogmatic. Algebraic geometers say 'ring' when they mean 'commutative ring', but this should not be taken as an argument for what is the correct definition of 'ring'. About the overloading of the word 'locally'. I agree it is overloaded, but by sneaking in further conditions the word is overloaded even more. About contrived vs. naturally occurring examples, I don't think it should influence the decision too much. (And who are we to judge what is contrived? Should the empty set count as a set? It was considered contrived for centuries.) (If in some situation it is important that a set is nonempty, it is a fair price to pay to say 'nonempty set' instead of just saying 'set'. If in some situation it is important that a locally cartesian closed category has a terminal object, it is surely not too much trouble to say 'locally cartesian closed category with a terminal object', given that in this example it is actually important.) (Speaking of empty: surely the empty category should count as locally cartesian closed :-) I am piling up parentheses in an effort to be social.) About local homeomorphisms, here are three related examples that I like: polynomial functors and cartesian maps, decomposition spaces and culf maps, Petri nets and etale maps. A general class of examples are Joyal's axiomatically defined classes of etale maps [see Joyal-Moerdijk: Completeness theorem for open maps]. They always form a locally cartesian closed category, generally not with a terminal object. Cheers, Joachim. PS: by 'nonempty' I meant 'inhabited', of course.