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