Are there important locally cartesian closed categories that actually are not cartesian closed?

In some (but not all) of the published definitions, a locally cartesian closed category is any category with all its slices cartesian closed. Such a category need not be cartesian closed itself, simply because it need not have a terminal object.

As a prominent example, there is the $n$-category Cafe: https://ncatlab.org/nlab/show/locally+cartesian+closed+category

I see how someone could find this a formally natural definition. In particular, someone might want to de-emphasize terminal objects for purposes of dependent type theory because terminal types are not very useful in programming even though they normally exist.

But I am curious to know if there are important examples of locally cartesian closed categories in this sense that actually do not have a terminal object (i.e. are actually not cartesian closed)?

One source of examples occurs to me: The disjoint union $C+D$ of any two cartesian closed categories $C,D$ is locally cartesian closed.

That does not look important to me, though I do not know it is not. There is a trivial embedding of that disjoint union as a pair of slice categories of a cartesian closed category. Formally adjoin a new terminal object for the whole disjoint union category, and add maps making the new terminal object into the disjoint union of the two previous terminal objects. But I cannot see this as an important kind of example, because to me this just looks like a presentation of the coproduct in the 2-category of toposes: which is realized by the product of the toposes in the 1-category of categories. (The objects $a,b$ of $C$ and $D$ appear as pairs $(a,1)$ and $(1,b)$ in the product, with the original terminal objects $1$.)

• Depending on what you mean by 'important' this is probably cheating (which is why I'm posting this as a comment, not an answer), but any discrete category with more than one object is LCCC but not CCC, and I'm sure you could cook up less trivial examples involving posets without greatest elements. – Clive Newstead Jul 28 '18 at 4:55
• @CliveNewstead Indeed, from a type theory perspective, lacking a terminal object makes it unclear what a "closed type/term" should be. Reading your "poset without greatest elements" suggestion logically analogously indicates that we're unable to state that some formula holds unconditionally. – Derek Elkins Jul 28 '18 at 4:58
• @DerekElkins: I take 'has a terminal object' to be part of the definition of LCCC when I'm doing semantics of type theory for more or less that reason; but a friend of mine once convinced me that the requirement that the distinguished object representing the 'empty context' be terminal is not necessary. (You can always make it terminal by taking the slice over that object!) – Clive Newstead Jul 28 '18 at 5:03
• @CliveNewstead Yes, in the parts of category theory I know best, making any object terminal by slicing over it is just "taking a generic element" defined over that object. I think I have seen this usage in (categorical) type theory but I am not expert on type theory. – Colin McLarty Jul 28 '18 at 5:08

The example most familiar to me is the category $\mathcal{LH}$ whose objects are topological spaces and whose morphisms are local homeomorphisms.
This category doesn't have a terminal object, but it is locally cartesian closed: each slice category $\mathcal{LH}/X$ is equivalent to the category of sheaves on $X$.