Somewhat wordy, but one could say "cartesian and locally cartesian closed category" or "globally and locally cartesian closed category" for one with a terminal object. On Wed, Jun 24, 2026 at 2:07 PM Jon Sterling via Categories < categories-list@categories.org.au> wrote:
Hi Emily,
Just a little thought. Personally I prefer that the definition leave out a terminal object, although I am sure that it may be possible to find examples of me in print having assumed it without mentioning it. My reason is twofold: first, consistency with one of the two main uses of "locally" in category theory; second, I think that even in type theory we over-emphasise the importance of the empty context (which does not arise in the *use* of dependent type theory, where all language is understood as taking place in some undetermined context anyway for the sake of substitution stability — and dependently typed internal languages can be used in semantic settings even when you don't have a terminal object).
As for a good name for lccc w/ terminal object, that I don't have an opinion on :)
Best, Jon
On Jun 24, 2026, at 2:19 PM, Emily Riehl via Categories < categories-list@categories.org.au> 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...
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
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