I think it makes sense for a "cartesian closed category" to include a terminal object, because (1) a "cartesian category" in the sense of one with finite products has a terminal object, and (2) a cartesian closed category is then a closed monoidal category. I see the argument that it would be more consistent with other uses of "locally" to leave the terminal object out of an LCCC. I think the main thing pushing me to include it is that examples of LCCCs without a terminal object are rather thin on the ground. I can think of very few that are not artificially contrived. If a "locally cartesian closed category" does include a terminal object, one could perhaps say "locally a cartesian closed category" (LACCC?) to mean one without a terminal object. On Wed, Jun 24, 2026 at 3:17 PM Henning Basold via Categories < categories-list@categories.org.au> wrote:
Dear Emily,
I don't feel that I can speak for the community, but let me point out that from the perspective of fibrations there are three things to consider:
1. In the realm of fibrations, a global terminal object is an extra piece of data that is not needed to define fibrations or quantifiers, and it arises by applying a truth functor (right adjoint to the fibration functor) to a terminal object of the base category. However, the definition of CCC in your book also includes a terminal object, which is also not strictly needed. Thus one can perhaps justify the addition of terminal objects by LCCC being a stronger set of assumptions altogether.
2. There are some subtleties around the example of injective maps on page 153. It is stated that reindexing can be either only along injective or along arbitrary maps. Applying the Grothendieck construction to the first choice yields the codomain fibration on Set_{mono}, which then has no global terminal object. Applying the Grothendieck construction to the second choice gives the subobject fibration over the category of all maps, which does have a global terminal object (truth predicate on a singleton set) and existential quantification uses the image factorisation system. Jacobs proves this in "Categorical Logic and Type Theory" in Theorem 4.4.4, and in Theorem 4.5.5 he shows that a finitely complete category is a logos if and only if the subobject fibration models first-order logic. Again, this suggests that terminal objects are additional data, but one may want to keep the space of models for LCCCs tight.
3. In the context of fibrations, it is natural to consider a setting of L -> C of a logic reasoning about terms in a calculus. Typically, C is forced to have finite products by taking contexts as objects and tuples of terms as morphisms. However, terms with a single variable would be easier as morphisms, but then the category has no products (unless the calculus admits products and terms are quotiented). Also sub-structural term calculi would not generally have products, even if one take context as objects and tuples of terms as morphisms. One may contemplate Cartesian logic on substructural calculi and aim to treat these using LCCC, in which case the terminal object/finite product assumption would be unnatural.
My personal preference is to add more adjectives where needed, or come up with a new name, as LCCC really suggests something on the fibres and not global.
Best,
Henning On 24/06/2026 15:19, Emily Riehl via Categories wrote:
There has been some discussion on the Category Theory zulip about the proper terminology for locally cartesian closed categories that I’d like to extend to the broader community.
https://categorytheory.zulipchat.com/#narrow/channel/229136-theory.3A-catego... <https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Fcategorytheory.zulipchat.com%2F%23narrow%2Fchannel%2F229136-theory.3A-category-theory%2Ftopic%2Flocally.20cartesian.20closed.20categories.20without.20a.20terminal.20objec%2Fwith%2F605614539&data=05%7C02%7Ch.basold%40liacs.leidenuniv.nl%7C618488a1c3354059b46d08ded2279f6f%7Cca2a7f76dbd74ec091086b3d524fb7c8%7C0%7C0%7C639179265051005320%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=EEi4Jt72AZ%2B9U0L9nWdwUbHkJ6SHqlqp1Y8q5jTsqDI%3D&reserved=0>
I raised this question because I have added a new section on locally cartesian closed categories as part of a revised second edition of *Category Theory in Context. *The current draft, can be found here and comments on this or anything else are very welcome (especially before the end of August, with sooner better than later):
https://emilyriehl.github.io/files/context.pdf <https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Femilyriehl.github.io%2Ffiles%2Fcontext.pdf&data=05%7C02%7Ch.basold%40liacs.leidenuniv.nl%7C618488a1c3354059b46d08ded2279f6f%7Cca2a7f76dbd74ec091086b3d524fb7c8%7C0%7C0%7C639179265051032640%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=HfvByw4gxlUfaJSbdnexzotn%2FhFjE14st8DqsHHVNRc%3D&reserved=0>
Does the community prefer reserving the term “locally cartesian closed categories” for the case where a terminal object exists (in addition to pullbacks)? If so, is there a good name for the version that is missing the terminal object? If not, is there a good name for the version that has a final limits?
As pointed out on the chat (h/t Nathanael Arkor) both conventions are widely used in the literature.
Thanks, Emily
PS: I was personally persuaded of the utility of the more general notion by the example of sets and monomorphisms. In the current draft of the text, I’m trying to provide intuition for some of the connections to logic without explicitly mentioning dependent type theory.
-- Kelly Miller Professor of Mathematics (she/her) Johns Hopkins University emilyriehl.github.io
_______________________________________________ Categories mailing list -- categories-list@categories.org.au To unsubscribe send an email to categories-list-leave@categories.org.au
_______________________________________________ Categories mailing list -- categories-list@categories.org.au To unsubscribe send an email to categories-list-leave@categories.org.au
-- Michael Shulman Professor of Mathematics for Humans <https://home.sandiego.edu/~shulman/humans.html> University of San Diego "The role of the intellectual cannot be to excuse the violence of one side and condemn that of the other." -- Albert Camus