Dear category theorists, The prefix "semi" is often used for weakening the axioms of a structure. A "semi-ring" is a ring where the additive structure is a commutative monoid. A "semi-monoid" (instead of "semi-group") is a monoid with or without a unit. The prefix "semi" is convenient and easy to remember. A "semi-LLC" could be a locally cartesian closed category with or without a terminal object. A "semi-topos" could be a topos with or without a terminal object. A "semi-cartesian category" could be a cartesian category with or without a terminal object. A "semi-monoidal category" could be a monoidal category with or without a unit object. Of course, there is no uniform procedure for weakening a structure in general. Best regards André ________________________________ De : Steve Awodey via Categories <categories-list@categories.org.au> Envoyé : 25 juin 2026 07:05 À : Categories List <categories-list@categories.org.au> Cc : Emily Riehl <eriehl@jhu.edu>; Jon Sterling <jon@jonmsterling.com>; Michael Shulman <shulman@sandiego.edu>; P.T. Johnstone <ptj1000@cam.ac.uk>; Steve Awodey <awodey@andrew.cmu.edu> Objet : [categories] Re: Terminology for locally cartesian closed categories, with and without a terminal object Friends, An example of an “LCCC\1” that I like is posets with discrete fibrations, because it’s easy to present when teaching semantics of type theory: simple types in Pos, then dependent types in dFib/P. This is also has the virtue of being “sufficient” for extensional MLTT (in the sense that the theory is *complete* with respect to the semantics) [1]. As for terminology, I’ll repeat my joke from the Zulip: if we include 1 in the definition of a locally cartesian closed category, then such near misses as dFib may be called "locally locally cartesian closed”. Categorical regards, Steve [1] S. Awodey and F. Rabe: Kripke Semantics for Martin-Löf's Extensional Type Theory. Logical Methods in Computer Science, Volume 7, Issue 3, 2011. https://doi.org/10.2168/LMCS-7(3:18)2011
On Jun 25, 2026, at 9:13 AM, P.T. Johnstone via Categories <categories-list@categories.org.au> wrote:
P {margin-top:0;margin-bottom:0;} Sorry to come late to this — I've been away for a couple of days.
When I wrote the first two parts of the Elephant, I thought quite a lot about terminological questions like this. For "locally cartesian closed", I decided to break the usual rule that "locally P" means "all slices have property P" but not that the category itself has P. The reason was that there is, as far as I know, only one not-wholly-artificial example of a category whose slices are all cartesian closed but which is not itself cc (namely the category of all topological spaces and local homeomorphisms); and it didn't seem worth burdening oneself with more complicated terminology for the sake of this one counterexample.
Peter Johnstone From: Michael Shulman via Categories <categories-list@categories.org.au> Sent: 24 June 2026 10:53 PM To: Jon Sterling via Categories <categories-list@categories.org.au> Cc: Emily Riehl <eriehl@jhu.edu>; Jon Sterling <jon@jonmsterling.com>; Michael Shulman <shulman@sandiego.edu> Subject: [categories] Re: Terminology for locally cartesian closed categories, with and without a terminal object 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 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
_______________________________________________ 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