Terminology for locally cartesian closed categories, with and without a terminal object
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
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
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
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<mailto: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<mailto: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<http://emilyriehl.github.io> _______________________________________________ Categories mailing list -- categories-list@categories.org.au<mailto:categories-list@categories.org.au> To unsubscribe send an email to categories-list-leave@categories.org.au<mailto:categories-list-leave@categories.org.au> _______________________________________________ Categories mailing list -- categories-list@categories.org.au<mailto:categories-list@categories.org.au> To unsubscribe send an email to categories-list-leave@categories.org.au<mailto: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
Dear Peter, There are many examples of Set-valued Galois theories where covering morphisms compose and locally form presheaf toposes. Or, note that the category of 'small' categories with morphisms being discrete fibrations is in the same relation with the presheaf toposes as the category of topological spaces and local homeomorphisms with the toposes of sheaves over topological spaces. Therefore, I would not say "only one not-wholly-artificial example". But I agree with your suggestion, and I would add the question: do we want every groupoid to be locally cartesian closed? Best regards, George ________________________________ From: P.T. Johnstone via Categories <categories-list@categories.org.au> Sent: Thursday, June 25, 2026 10:13 To: Michael Shulman via Categories <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> Subject: [categories] Re: Terminology for locally cartesian closed categories, with and without a terminal object CAUTION: This email originated outside the UCT network. Do not click any links or open attachments unless you know and trust the source. 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<mailto: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<mailto: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-category-theory/topic/locally.20cartesian.20closed.20categories.20without.20a.20terminal.20objec/with/605614539<https://categorytheory.zulipchat.com/#narrow/channel/229136-theory.3A-category-theory/topic/locally.20cartesian.20closed.20categories.20without.20a.20terminal.20objec/with/605614539> 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://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<http://emilyriehl.github.io> _______________________________________________ Categories mailing list -- categories-list@categories.org.au<mailto:categories-list@categories.org.au> To unsubscribe send an email to categories-list-leave@categories.org.au<mailto:categories-list-leave@categories.org.au> _______________________________________________ Categories mailing list -- categories-list@categories.org.au<mailto:categories-list@categories.org.au> To unsubscribe send an email to categories-list-leave@categories.org.au<mailto: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 Disclaimer - University of Cape Town This email is subject to UCT policies and email disclaimer published on our website at https://www.uct.ac.za/main/email-disclaimer or obtainable from +27 21 650 9111. If this email is not related to the business of UCT, it is sent by the sender in an individual capacity. Please report security incidents or abuse via https://csirt.uct.ac.za/report-incident
1) I think that "Locally Cartesian Closed" is perfect for the notion that does not require existence of a terminal object. What about non connected categories ? 2) Discrete fibrations and Set-valued functors are the same thing. The category of elements and the clasical definition of a Set valued functor are just two ways of codifying the same information, data. best regards Eduardo Dubuc On 25/06/2026 07:13, George Janelidze via Categories wrote:
Dear Peter,
There are many examples of Set-valued Galois theories where covering morphisms compose and locally form presheaf toposes. Or, note that the category of 'small' categories with morphisms being discrete fibrations is in the same relation with the presheaf toposes as the category of topological spaces and local homeomorphisms with the toposes of sheaves over topological spaces. Therefore, I would not say "only one not- wholly-artificial example".
But I agree with your suggestion, and I would add the question: do we want every groupoid to be locally cartesian closed?
Best regards, George
------------------------------------------------------------------------ *From:* P.T. Johnstone via Categories <categories-list@categories.org.au> *Sent:* Thursday, June 25, 2026 10:13 *To:* Michael Shulman via Categories <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> *Subject:* [categories] Re: Terminology for locally cartesian closed categories, with and without a terminal object
CAUTION: This email originated outside the UCT network. Do not click any links or open attachments unless you know and trust the source.
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 <mailto: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 <mailto: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-category-theory/topic/ locally.20cartesian.20closed.20categories.20without.20a.20terminal.20objec/with/605614539 <https://categorytheory.zulipchat.com/#narrow/channel/229136-theory.3A-category-theory/topic/locally.20cartesian.20closed.20categories.20without.20a.20terminal.20objec/with/605614539>
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:// 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 <http://emilyriehl.github.io>
_______________________________________________ Categories mailing list -- categories-list@categories.org.au <mailto:categories-list@categories.org.au> To unsubscribe send an email to categories-list- leave@categories.org.au <mailto:categories-list- leave@categories.org.au>
_______________________________________________ Categories mailing list -- categories-list@categories.org.au <mailto:categories-list@categories.org.au> To unsubscribe send an email to categories-list- leave@categories.org.au <mailto: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
Disclaimer - University of Cape Town This email is subject to UCT policies and email disclaimer published on our website at https:// www.uct.ac.za/main/email-disclaimer or obtainable from +27 21 650 9111. If this email is not related to the business of UCT, it is sent by the sender in an individual capacity. Please report security incidents or abuse via https://csirt.uct.ac.za/report-incident
_______________________________________________ Categories mailing list -- categories-list@categories.org.au To unsubscribe send an email to categories-list-leave@categories.org.au
Dear Eduardo, I disagree with your item "1)", but at least I understand it. However, I don't understand your item "2)": Are you just saying that establishing an equivalence between the category of discrete fibrations over a category C and the category of functors C^{op}—>Set is EASIER than establishing an equivalence between the category of local homeomorphisms with codomain X and the category of sheaves of sets over X? Well, yes, it is much easier, but why are you saying that? Best regards, George ________________________________ From: Eduardo Dubuc <edubuc@dm.uba.ar> Sent: Thursday, June 25, 2026 19:32 To: George Janelidze via Categories <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>; George Janelidze <george.janelidze@uct.ac.za> Subject: Re: [categories] Re: Terminology for locally cartesian closed categories, with and without a terminal object CAUTION: This email originated outside the UCT network. Do not click any links or open attachments unless you know and trust the source. 1) I think that "Locally Cartesian Closed" is perfect for the notion that does not require existence of a terminal object. What about non connected categories ? 2) Discrete fibrations and Set-valued functors are the same thing. The category of elements and the clasical definition of a Set valued functor are just two ways of codifying the same information, data. best regards Eduardo Dubuc On 25/06/2026 07:13, George Janelidze via Categories wrote:
Dear Peter,
There are many examples of Set-valued Galois theories where covering morphisms compose and locally form presheaf toposes. Or, note that the category of 'small' categories with morphisms being discrete fibrations is in the same relation with the presheaf toposes as the category of topological spaces and local homeomorphisms with the toposes of sheaves over topological spaces. Therefore, I would not say "only one not- wholly-artificial example".
But I agree with your suggestion, and I would add the question: do we want every groupoid to be locally cartesian closed?
Best regards, George
------------------------------------------------------------------------ *From:* P.T. Johnstone via Categories <categories-list@categories.org.au> *Sent:* Thursday, June 25, 2026 10:13 *To:* Michael Shulman via Categories <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> *Subject:* [categories] Re: Terminology for locally cartesian closed categories, with and without a terminal object
CAUTION: This email originated outside the UCT network. Do not click any links or open attachments unless you know and trust the source.
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 <mailto: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 <mailto: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-<https://categorytheory.zulipchat.com/#narrow/channel/229136-> theory.3A-category-theory/topic/ locally.20cartesian.20closed.20categories.20without.20a.20terminal.20objec/with/605614539 <https://categorytheory.zulipchat.com/#narrow/channel/229136-theory.3A-category-theory/topic/locally.20cartesian.20closed.20categories.20without.20a.20terminal.20objec/with/605614539<https://categorytheory.zulipchat.com/#narrow/channel/229136-theory.3A-category-theory/topic/locally.20cartesian.20closed.20categories.20without.20a.20terminal.20objec/with/605614539>>
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://emilyriehl.github.io/files/context.pdf> <https:// emilyriehl.github.io/files/context.pdf<http://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 <http://emilyriehl.github.io<http://emilyriehl.github.io>>
_______________________________________________ Categories mailing list -- categories-list@categories.org.au <mailto:categories-list@categories.org.au> To unsubscribe send an email to categories-list- leave@categories.org.au <mailto:categories-list- leave@categories.org.au>
_______________________________________________ Categories mailing list -- categories-list@categories.org.au <mailto:categories-list@categories.org.au> To unsubscribe send an email to categories-list- leave@categories.org.au <mailto:categories-list-leave@categories.org.au>
-- Michael Shulman Professor of Mathematics for Humans <https://home.sandiego.edu/~shulman/<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
Disclaimer - University of Cape Town This email is subject to UCT policies and email disclaimer published on our website at https:// www.uct.ac.za/main/email-disclaimer<http://www.uct.ac.za/main/email-disclaimer> or obtainable from +27 21 650 9111. If this email is not related to the business of UCT, it is sent by the sender in an individual capacity. Please report security incidents or abuse via https://csirt.uct.ac.za/report-incident<https://csirt.uct.ac.za/report-incident>
_______________________________________________ Categories mailing list -- categories-list@categories.org.au To unsubscribe send an email to categories-list-leave@categories.org.au Disclaimer - University of Cape Town This email is subject to UCT policies and email disclaimer published on our website at https://www.uct.ac.za/main/email-disclaimer or obtainable from +27 21 650 9111. If this email is not related to the business of UCT, it is sent by the sender in an individual capacity. Please report security incidents or abuse via https://csirt.uct.ac.za/report-incident
Dear George, thanks for your reply, I clarify for evrybody: In the item 2) I observe that the clasical definition of a Set-valued functor as the data of the action of a category on a family of sets, is the same that the data in the definition of discrete fibration. They are just two ways of codifying the same information: Action of a Category = Discrete Fibration The axioms on this data correspond. best regards On 25/06/2026 15:10, George Janelidze wrote:
Dear Eduardo,
I disagree with your item "1)", but at least I understand it.
However, I don't understand your item "2)": Are you just saying that establishing an equivalence between the category of discrete fibrations over a category C and the category of functors C^{op}—>Set is EASIER than establishing an equivalence between the category of local homeomorphisms with codomain X and the category of sheaves of sets over X? Well, yes, it is much easier, but why are you saying that?
Best regards, George
------------------------------------------------------------------------ *From:* Eduardo Dubuc <edubuc@dm.uba.ar> *Sent:* Thursday, June 25, 2026 19:32 *To:* George Janelidze via Categories <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>; George Janelidze <george.janelidze@uct.ac.za> *Subject:* Re: [categories] Re: Terminology for locally cartesian closed categories, with and without a terminal object
CAUTION: This email originated outside the UCT network. Do not click any links or open attachments unless you know and trust the source.
1) I think that "Locally Cartesian Closed" is perfect for the notion that does not require existence of a terminal object. What about non connected categories ?
2) Discrete fibrations and Set-valued functors are the same thing. The category of elements and the clasical definition of a Set valued functor are just two ways of codifying the same information, data.
best regards Eduardo Dubuc
Dear Peter,
There are many examples of Set-valued Galois theories where covering morphisms compose and locally form presheaf toposes. Or, note that the category of 'small' categories with morphisms being discrete fibrations is in the same relation with the presheaf toposes as the category of topological spaces and local homeomorphisms with the toposes of sheaves over topological spaces. Therefore, I would not say "only one not- wholly-artificial example".
But I agree with your suggestion, and I would add the question: do we want every groupoid to be locally cartesian closed?
Best regards, George
------------------------------------------------------------------------ *From:* P.T. Johnstone via Categories <categories-list@categories.org.au> *Sent:* Thursday, June 25, 2026 10:13 *To:* Michael Shulman via Categories <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> *Subject:* [categories] Re: Terminology for locally cartesian closed categories, with and without a terminal object
CAUTION: This email originated outside the UCT network. Do not click any links or open attachments unless you know and trust the source.
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-
On 25/06/2026 07:13, George Janelidze via Categories wrote: 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 <mailto: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 <mailto: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- <https://categorytheory.zulipchat.com/#narrow/channel/229136-> theory.3A-category-theory/topic/
locally.20cartesian.20closed.20categories.20without.20a.20terminal.20objec/with/605614539 <https://categorytheory.zulipchat.com/#narrow/channel/229136-theory.3A-catego... <https://categorytheory.zulipchat.com/#narrow/channel/229136-theory.3A-category-theory/topic/locally.20cartesian.20closed.20categories.20without.20a.20terminal.20objec/with/605614539>>
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):
emilyriehl.github.io/files/context.pdf <http://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 <http://emilyriehl.github.io <http:// emilyriehl.github.io>>
_______________________________________________ Categories mailing list -- categories-list@categories.org.au <mailto:categories-list@categories.org.au> To unsubscribe send an email to categories-list- leave@categories.org.au <mailto:categories-list- leave@categories.org.au>
_______________________________________________ Categories mailing list -- categories-list@categories.org.au <mailto:categories-list@categories.org.au> To unsubscribe send an email to categories-list- leave@categories.org.au <mailto:categories-list-leave@categories.org.au>
-- Michael Shulman Professor of Mathematics for Humans <https://home.sandiego.edu/ ~shulman/ <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
Disclaimer - University of Cape Town This email is subject to UCT policies and email disclaimer published on our website at https:// www.uct.ac.za/main/email-disclaimer <http://www.uct.ac.za/main/email- disclaimer> or obtainable from +27 21 650 9111. If this email is not related to the business of UCT, it is sent by the sender in an individual capacity. Please report security incidents or abuse via https://csirt.uct.ac.za/report-incident <https:// csirt.uct.ac.za/report-incident>
_______________________________________________ Categories mailing list -- categories-list@categories.org.au To unsubscribe send an email to categories-list-leave@categories.org.au Disclaimer - University of Cape Town This email is subject to UCT
emilyriehl.github.io/files/context.pdf> <https:// policies and email disclaimer published on our website at https:// www.uct.ac.za/main/email-disclaimer or obtainable from +27 21 650 9111. If this email is not related to the business of UCT, it is sent by the sender in an individual capacity. Please report security incidents or abuse via https://csirt.uct.ac.za/report-incident
Dear Eduardo, Thank you, but may I gently ask again? Let us begin with families of sets. We might define an I-indexed family of sets as a map from I to the class of all sets, or we might define it as a pair (A,p) where p is a map from A to I. These two definitions are fundamentally different: for example, the first definition does not make members of the family disjoint while the second one does. These two definitions produce two different categories, which, however, are equivalent to each other. And the story of discrete fibrations and Set-valued functors is essentially the same. And even the story of sheaves over a space X and local homeomorphisms A—>X is also essentially the same. Now, what do we mean by "the same data"? Is it just a about a canonical equivalence of categories? If yes, then I'll immediately insist that a local homeomorphism is the same data as a sheaf. By the way, Steve Awodey was mentioning disctere fibrations of posets, and so let me mention that discrete fibrations of preorders are same (in a stronger sense!) as local homeomorphisms of finite topological spaces (and, as we know, posets are nothing but preorders with T0). I would go even further and say discrete fibrations, actions, and Set-valued functors form three (equivalent but) pairwise different categories — and is not this something we always explain to students? With apologies for making trivial remarks and Best regards, George ________________________________ From: Eduardo Dubuc <edubuc@dm.uba.ar> Sent: Thursday, June 25, 2026 20:56 To: George Janelidze <george.janelidze@uct.ac.za>; George Janelidze via Categories <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> Subject: Re: [categories] Re: Terminology for locally cartesian closed categories, with and without a terminal object CAUTION: This email originated outside the UCT network. Do not click any links or open attachments unless you know and trust the source. Dear George, thanks for your reply, I clarify for evrybody: In the item 2) I observe that the clasical definition of a Set-valued functor as the data of the action of a category on a family of sets, is the same that the data in the definition of discrete fibration. They are just two ways of codifying the same information: Action of a Category = Discrete Fibration The axioms on this data correspond. best regards On 25/06/2026 15:10, George Janelidze wrote:
Dear Eduardo,
I disagree with your item "1)", but at least I understand it.
However, I don't understand your item "2)": Are you just saying that establishing an equivalence between the category of discrete fibrations over a category C and the category of functors C^{op}—>Set is EASIER than establishing an equivalence between the category of local homeomorphisms with codomain X and the category of sheaves of sets over X? Well, yes, it is much easier, but why are you saying that?
Best regards, George
------------------------------------------------------------------------ *From:* Eduardo Dubuc <edubuc@dm.uba.ar> *Sent:* Thursday, June 25, 2026 19:32 *To:* George Janelidze via Categories <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>; George Janelidze <george.janelidze@uct.ac.za> *Subject:* Re: [categories] Re: Terminology for locally cartesian closed categories, with and without a terminal object
CAUTION: This email originated outside the UCT network. Do not click any links or open attachments unless you know and trust the source.
1) I think that "Locally Cartesian Closed" is perfect for the notion that does not require existence of a terminal object. What about non connected categories ?
2) Discrete fibrations and Set-valued functors are the same thing. The category of elements and the clasical definition of a Set valued functor are just two ways of codifying the same information, data.
best regards Eduardo Dubuc
Dear Peter,
There are many examples of Set-valued Galois theories where covering morphisms compose and locally form presheaf toposes. Or, note that the category of 'small' categories with morphisms being discrete fibrations is in the same relation with the presheaf toposes as the category of topological spaces and local homeomorphisms with the toposes of sheaves over topological spaces. Therefore, I would not say "only one not- wholly-artificial example".
But I agree with your suggestion, and I would add the question: do we want every groupoid to be locally cartesian closed?
Best regards, George
------------------------------------------------------------------------ *From:* P.T. Johnstone via Categories <categories-list@categories.org.au> *Sent:* Thursday, June 25, 2026 10:13 *To:* Michael Shulman via Categories <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> *Subject:* [categories] Re: Terminology for locally cartesian closed categories, with and without a terminal object
CAUTION: This email originated outside the UCT network. Do not click any links or open attachments unless you know and trust the source.
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-
On 25/06/2026 07:13, George Janelidze via Categories wrote: 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 <mailto: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 <mailto: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-<https://categorytheory.zulipchat.com/#narrow/channel/229136-> <https://categorytheory.zulipchat.com/#narrow/channel/229136-<https://categorytheory.zulipchat.com/#narrow/channel/229136->> theory.3A-category-theory/topic/
locally.20cartesian.20closed.20categories.20without.20a.20terminal.20objec/with/605614539 <https://categorytheory.zulipchat.com/#narrow/channel/229136-theory.3A-category-theory/topic/locally.20cartesian.20closed.20categories.20without.20a.20terminal.20objec/with/605614539<https://categorytheory.zulipchat.com/#narrow/channel/229136-theory.3A-category-theory/topic/locally.20cartesian.20closed.20categories.20without.20a.20terminal.20objec/with/605614539> <https://categorytheory.zulipchat.com/#narrow/channel/229136-theory.3A-category-theory/topic/locally.20cartesian.20closed.20categories.20without.20a.20terminal.20objec/with/605614539<https://categorytheory.zulipchat.com/#narrow/channel/229136-theory.3A-category-theory/topic/locally.20cartesian.20closed.20categories.20without.20a.20terminal.20objec/with/605614539>>>
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://emilyriehl.github.io/files/context.pdf> <https://
emilyriehl.github.io/files/context.pdf<http://emilyriehl.github.io/files/context.pdf> <http://emilyriehl.github.io/<http://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 <http://emilyriehl.github.io<http://emilyriehl.github.io> <http:// emilyriehl.github.io>>
_______________________________________________ Categories mailing list -- categories-list@categories.org.au <mailto:categories-list@categories.org.au> To unsubscribe send an email to categories-list- leave@categories.org.au <mailto:categories-list- leave@categories.org.au>
_______________________________________________ Categories mailing list -- categories-list@categories.org.au <mailto:categories-list@categories.org.au> To unsubscribe send an email to categories-list- leave@categories.org.au <mailto:categories-list-leave@categories.org.au>
-- Michael Shulman Professor of Mathematics for Humans <https://home.sandiego.edu/<https://home.sandiego.edu> ~shulman/ <https://home.sandiego.edu/~shulman<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
Disclaimer - University of Cape Town This email is subject to UCT policies and email disclaimer published on our website at https:// www.uct.ac.za/main/email-disclaimer<http://www.uct.ac.za/main/email-disclaimer> <http://www.uct.ac.za/main/email-<http://www.uct.ac.za/main/email-> disclaimer> or obtainable from +27 21 650 9111. If this email is not related to the business of UCT, it is sent by the sender in an individual capacity. Please report security incidents or abuse via https://csirt.uct.ac.za/report-incident<https://csirt.uct.ac.za/report-incident> <https:// csirt.uct.ac.za/report-incident<http://csirt.uct.ac.za/report-incident>>
_______________________________________________ Categories mailing list -- categories-list@categories.org.au To unsubscribe send an email to categories-list-leave@categories.org.au Disclaimer - University of Cape Town This email is subject to UCT
emilyriehl.github.io/files/context.pdf<http://emilyriehl.github.io/files/context.pdf>> <https:// policies and email disclaimer published on our website at https:// www.uct.ac.za/main/email-disclaimer<http://www.uct.ac.za/main/email-disclaimer> or obtainable from +27 21 650 9111. If this email is not related to the business of UCT, it is sent by the sender in an individual capacity. Please report security incidents or abuse via https://csirt.uct.ac.za/report-incident<https://csirt.uct.ac.za/report-incident> Disclaimer - University of Cape Town This email is subject to UCT policies and email disclaimer published on our website at https://www.uct.ac.za/main/email-disclaimer or obtainable from +27 21 650 9111. If this email is not related to the business of UCT, it is sent by the sender in an individual capacity. Please report security incidents or abuse via https://csirt.uct.ac.za/report-incident
I think the following are also examples: - the category of Sets and monomorphisms. More generally, if C is an lccc (in the weaker sense), and (E,M) is a factorisation system on C for which E-maps are stable under pullbacks along M-maps, then I think the category of C-objects and M-maps is an lccc (in the weaker sense), but will normally not have a terminal object. - the category of arrows in Set and pullback squares. More generally, if C is an lccc (in the weaker sense) and E ---> C is a fibration, then I think E_cart (E-objects and cartesian maps) is lccc (in the weaker sense) but will normally not have a terminal object. Richard George Janelidze via Categories <categories-list@categories.org.au> writes:
Dear Peter,
There are many examples of Set-valued Galois theories where covering morphisms compose and locally form presheaf toposes. Or, note that the category of 'small' categories with morphisms being discrete fibrations is in the same relation with the presheaf toposes as the category of topological spaces and local homeomorphisms with the toposes of sheaves over topological spaces. Therefore, I would not say "only one not-wholly-artificial example".
But I agree with your suggestion, and I would add the question: do we want every groupoid to be locally cartesian closed?
Best regards, George
------------------------------------------------------------------------------- From: P.T. Johnstone via Categories <categories-list@categories.org.au> Sent: Thursday, June 25, 2026 10:13 To: Michael Shulman via Categories <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> Subject: [categories] Re: Terminology for locally cartesian closed categories, with and without a terminal object
CAUTION: This email originated outside the UCT network. Do not click any links or open attachments unless you know and trust the source.
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.
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
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
Dear categorical friends, The prefix "semi" is often used for weakening the axioms of a structure. A "semi-ring" is a ring in which the additive structure is a commutative monoid with or without inverses. We may say "semi-monoid" (instead of "semi-group") for a monoid with or without a unit. We may say "semi-LLC" for a locally cartesian closed category with or without a terminal object. Similarly, we could also say "semi-topos" for a topos with or without a terminal object. Also say "semi-cartesian category" for a cartesian category with or without a terminal object. We might say "semi-monoidal category" for a monoidal category with or without a unit object. The prefix "semi" is convenient and easy to remember. 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
The terminology "locally" has never been very lucky. Consider e.g. "locally compact (topological) space". (1) Some people say: every point has a compact neighbourhood. (2) Other people say: every neighbourhood of a point has a compact neighbourhood of the point. The approach (1) works for Hausdorff spaces only, where the condition (1) implies (2). In the absence of the Hausdorff condition, it gives spurious conclusions with no real meaning. It is (2) that is right. But if you dig further, the right ultimate condition is that the open sets form a continuous lattice. "locally" seems to be used as inconsistently in category theory as it is used in point-set topology. If I could vote, I would vote for the real meaning of locality, and say that the slices satisfy the property. Any thing more or less should be added or subtracted from the terminology with further adjectives. Otherwise we get an ad hoc scaffolding of terminology. Locality in itself, both in topology and in category theory, is an important notion. It shouldn't be distorted by the coincidences of the theorems we want to prove about it, or the examples we happen to have. M.
Just one more thing: remember that a locally compact space doesn't need to be compact. The same thing is happening here with local cartesian closedness. M. On 25/06/2026 23:08, Martin Escardo wrote:
The terminology "locally" has never been very lucky.
Consider e.g. "locally compact (topological) space".
(1) Some people say: every point has a compact neighbourhood.
(2) Other people say: every neighbourhood of a point has a compact neighbourhood of the point.
The approach (1) works for Hausdorff spaces only, where the condition (1) implies (2). In the absence of the Hausdorff condition, it gives spurious conclusions with no real meaning.
It is (2) that is right. But if you dig further, the right ultimate condition is that the open sets form a continuous lattice.
"locally" seems to be used as inconsistently in category theory as it is used in point-set topology.
If I could vote, I would vote for the real meaning of locality, and say that the slices satisfy the property. Any thing more or less should be added or subtracted from the terminology with further adjectives. Otherwise we get an ad hoc scaffolding of terminology.
Locality in itself, both in topology and in category theory, is an important notion. It shouldn't be distorted by the coincidences of the theorems we want to prove about it, or the examples we happen to have.
M.
On Thu, Jun 25, 2026 at 4:15 PM Martin Escardo via Categories < categories-list@categories.org.au> wrote:
Just one more thing: remember that a locally compact space doesn't need to be compact.
Indeed, and a locally connected space need not be connected, nor need a connected space be locally connected, so one not infrequently reasons about "connected and locally connected" or "globally and locally connected" spaces. So the suggestion of "cartesian and locally cartesian closed" or "globally and locally cartesian closed" for the version with terminal object would match that pattern. And they're even both about the terminal object: a locally connected topos is connected iff the left adjoint of the inverse image of its global sections preserves the terminal object.
The same thing is happening here with local cartesian closedness.
M.
On 25/06/2026 23:08, Martin Escardo wrote:
The terminology "locally" has never been very lucky.
Consider e.g. "locally compact (topological) space".
(1) Some people say: every point has a compact neighbourhood.
(2) Other people say: every neighbourhood of a point has a compact neighbourhood of the point.
The approach (1) works for Hausdorff spaces only, where the condition (1) implies (2). In the absence of the Hausdorff condition, it gives spurious conclusions with no real meaning.
It is (2) that is right. But if you dig further, the right ultimate condition is that the open sets form a continuous lattice.
"locally" seems to be used as inconsistently in category theory as it is used in point-set topology.
If I could vote, I would vote for the real meaning of locality, and say that the slices satisfy the property. Any thing more or less should be added or subtracted from the terminology with further adjectives. Otherwise we get an ad hoc scaffolding of terminology.
Locality in itself, both in topology and in category theory, is an important notion. It shouldn't be distorted by the coincidences of the theorems we want to prove about it, or the examples we happen to have.
M.
_______________________________________________ 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
Isn't terminology fun? On 26 Jun 2026, at 8:08 am, Martin Escardo via Categories <categories-list@categories.org.au> wrote: The terminology "locally" has never been very lucky. I agree with Martin. The term "local" is the culprit. Here I go dragging things out of my memory. Jon Beck, Myles Tierney and others, as far back as 1968, were pushing for explicit terminology especially when the explicit term was just as short. For example, "category C is locally P" was being used to mean "each hom of C has property P". In SLNM47, Jean Bénabou introduced the local terminology for homs of bicategories. Yet Jon and Myles would prefer "small homs" to "locally small", for example. Bill Lawvere was using the term "(bi)closed bicategory" when composing with a 1-morphism had a right adjoint (so a one-object bicategory is closed iff it is as a monoidal category). In SLNM420 page 66, Brian Day says a category C with finite limits is a "closed span category" when each slice C/c is cartesian closed. I think this was a nod to both Jean and Bill by moving from the finitely complete C to the bicategory Span(C): cartesian closed slices amounts to both Span(C) closed in the Bill sense and to locally closed in the Jean sense. Having the homs of Span(C) cartesian closed when C merely has pullbacks, is also interesting. Ross
Dear Ross This discussion reminded me of your paper with Aurelio called (I think) Order Ideals. I always liked your regular categories without 1 (regular epi. monic span factorization of spans and so on). It was obvious then and now that it was a better set-up for studying "relations". I wanted to build on that approach for the Cartesian Bicategories stuff with (in those days) Max and Aurelio. Of course it was not to be. Max was far too into his own thoughts on regular categories and, in spite of being a coauthor of Order Ideals, Aurelio wanted no part of it because if you chuck 1 then you really can't call what's left a Cartesian Bicategory and the name was very important to him. But it would also be good to look at the things Bill did in his Diagonal Arguments paper to see if the absence of 1 suggests some new concepts and theorems as deep as the ones you obviously lose. Very best Richard ________________________________ From: Ross Street via Categories <categories-list@categories.org.au> Sent: June 26, 2026 03:56 To: categories-list@categories.org.au <categories-list@categories.org.au> Cc: Ross Street <ross.street@mq.edu.au> Subject: [categories] Re: Terminology for locally cartesian closed categories, with and without a terminal object CAUTION: The Sender of this email is not from within Dalhousie. Isn't terminology fun? On 26 Jun 2026, at 8:08 am, Martin Escardo via Categories <categories-list@categories.org.au> wrote: The terminology "locally" has never been very lucky. I agree with Martin. The term "local" is the culprit. Here I go dragging things out of my memory. Jon Beck, Myles Tierney and others, as far back as 1968, were pushing for explicit terminology especially when the explicit term was just as short. For example, "category C is locally P" was being used to mean "each hom of C has property P". In SLNM47, Jean Bénabou introduced the local terminology for homs of bicategories. Yet Jon and Myles would prefer "small homs" to "locally small", for example. Bill Lawvere was using the term "(bi)closed bicategory" when composing with a 1-morphism had a right adjoint (so a one-object bicategory is closed iff it is as a monoidal category). In SLNM420 page 66, Brian Day says a category C with finite limits is a "closed span category" when each slice C/c is cartesian closed. I think this was a nod to both Jean and Bill by moving from the finitely complete C to the bicategory Span(C): cartesian closed slices amounts to both Span(C) closed in the Bill sense and to locally closed in the Jean sense. Having the homs of Span(C) cartesian closed when C merely has pullbacks, is also interesting. Ross
Hi Emily and everybody if something should be called 'locally cartesian closed category', I think we should at least read the words and ponder what they say. Those four words do not imply anything about a terminal object (just as they do not suggest the existence of finite sums). I am surprised this is not the end of the discussion, but we are a very social community :-) It seems that the only argument in favour of sneaking in the extra condition of having a terminal object is that the phrase has been used in that way in the past, even in a very authoritative source like the Elephant. I don't think that argument should be given much weight. Peter already admitted it was laziness. He said that there was a terminal object in all examples known to him -- except one example which he decided to exclude, cold-bloodedly :-) I don't mean to criticise the Elephant -- let alone its author! It is fine to repurpose terminology a bit, without being dogmatic. Algebraic geometers say 'ring' when they mean 'commutative ring', but this should not be taken as an argument for what is the correct definition of 'ring'. About the overloading of the word 'locally'. I agree it is overloaded, but by sneaking in further conditions the word is overloaded even more. About contrived vs. naturally occurring examples, I don't think it should influence the decision too much. (And who are we to judge what is contrived? Should the empty set count as a set? It was considered contrived for centuries.) (If in some situation it is important that a set is nonempty, it is a fair price to pay to say 'nonempty set' instead of just saying 'set'. If in some situation it is important that a locally cartesian closed category has a terminal object, it is surely not too much trouble to say 'locally cartesian closed category with a terminal object', given that in this example it is actually important.) (Speaking of empty: surely the empty category should count as locally cartesian closed :-) I am piling up parentheses in an effort to be social.) About local homeomorphisms, here are three related examples that I like: polynomial functors and cartesian maps, decomposition spaces and culf maps, Petri nets and etale maps. A general class of examples are Joyal's axiomatically defined classes of etale maps [see Joyal-Moerdijk: Completeness theorem for open maps]. They always form a locally cartesian closed category, generally not with a terminal object. Cheers, Joachim. PS: by 'nonempty' I meant 'inhabited', of course.
Dear Joachim, I enjoyed very much your posting !, beautiful style of writing, and settling definitively the question (1 or not 1) on the side that existence of a terminal object should not be part of the definition of a locally cartesian closed category. Congratulations, Eduardo On 27/06/2026 06:07, Joachim Kock via Categories wrote:
Hi Emily and everybody
if something should be called 'locally cartesian closed category', I think we should at least read the words and ponder what they say. Those four words do not imply anything about a terminal object (just as they do not suggest the existence of finite sums).
I am surprised this is not the end of the discussion, but we are a very social community :-)
It seems that the only argument in favour of sneaking in the extra condition of having a terminal object is that the phrase has been used in that way in the past, even in a very authoritative source like the Elephant.
I don't think that argument should be given much weight.
Peter already admitted it was laziness. He said that there was a terminal object in all examples known to him -- except one example which he decided to exclude, cold-bloodedly :-)
I don't mean to criticise the Elephant -- let alone its author! It is fine to repurpose terminology a bit, without being dogmatic. Algebraic geometers say 'ring' when they mean 'commutative ring', but this should not be taken as an argument for what is the correct definition of 'ring'.
About the overloading of the word 'locally'. I agree it is overloaded, but by sneaking in further conditions the word is overloaded even more.
About contrived vs. naturally occurring examples, I don't think it should influence the decision too much. (And who are we to judge what is contrived? Should the empty set count as a set? It was considered contrived for centuries.) (If in some situation it is important that a set is nonempty, it is a fair price to pay to say 'nonempty set' instead of just saying 'set'. If in some situation it is important that a locally cartesian closed category has a terminal object, it is surely not too much trouble to say 'locally cartesian closed category with a terminal object', given that in this example it is actually important.) (Speaking of empty: surely the empty category should count as locally cartesian closed :-) I am piling up parentheses in an effort to be social.)
About local homeomorphisms, here are three related examples that I like: polynomial functors and cartesian maps, decomposition spaces and culf maps, Petri nets and etale maps. A general class of examples are Joyal's axiomatically defined classes of etale maps [see Joyal-Moerdijk: Completeness theorem for open maps]. They always form a locally cartesian closed category, generally not with a terminal object.
Cheers, Joachim.
PS: by 'nonempty' I meant 'inhabited', of course.
_______________________________________________ Categories mailing list -- categories-list@categories.org.au To unsubscribe send an email to categories-list-leave@categories.org.au
Dear Peter, Your remark about there being "only one not-wholly-artificial example" of a category with cartesian closed slices but not itself cartesian closed resonates with a concrete structure from my recent work on agent memory systems. The Genesis primitive is an operation category with an initial object (the empty operation sequence, ε). The category is generally open-ended — the agent is still running, so there is no terminal object. Simultaneously, the Stratification primitive is a Grothendieck opfibration over a base of memory-layer codes. The fibres are well-behaved while the total category carries no global terminal object — exactly the pattern Richard Garner described in his examples of Sets with monomorphisms and Cartesian maps in a fibration. The full formal apparatus — a partial Horn axiomatisation over a finite many-sorted signature, a computational rewrite core, and modular independence proofs for the three primitive roles — is developed in a companion technical report, available at https://zenodo.org/records/20364778 . Best regards, Abdiel Mars Eduardo Dubuc via Categories <categories-list@categories.org.au> 于2026年6月28日周日 04:54写道：
Dear Joachim, I enjoyed very much your posting !, beautiful style of writing, and settling definitively the question (1 or not 1) on the side that existence of a terminal object should not be part of the definition of a locally cartesian closed category.
Congratulations, Eduardo
On 27/06/2026 06:07, Joachim Kock via Categories wrote:
Hi Emily and everybody
if something should be called 'locally cartesian closed category', I think we should at least read the words and ponder what they say. Those four words do not imply anything about a terminal object (just as they do not suggest the existence of finite sums).
I am surprised this is not the end of the discussion, but we are a very social community :-)
It seems that the only argument in favour of sneaking in the extra condition of having a terminal object is that the phrase has been used in that way in the past, even in a very authoritative source like the Elephant.
I don't think that argument should be given much weight.
Peter already admitted it was laziness. He said that there was a terminal object in all examples known to him -- except one example which he decided to exclude, cold-bloodedly :-)
I don't mean to criticise the Elephant -- let alone its author! It is fine to repurpose terminology a bit, without being dogmatic. Algebraic geometers say 'ring' when they mean 'commutative ring', but this should not be taken as an argument for what is the correct definition of 'ring'.
About the overloading of the word 'locally'. I agree it is overloaded, but by sneaking in further conditions the word is overloaded even more.
About contrived vs. naturally occurring examples, I don't think it should influence the decision too much. (And who are we to judge what is contrived? Should the empty set count as a set? It was considered contrived for centuries.) (If in some situation it is important that a set is nonempty, it is a fair price to pay to say 'nonempty set' instead of just saying 'set'. If in some situation it is important that a locally cartesian closed category has a terminal object, it is surely not too much trouble to say 'locally cartesian closed category with a terminal object', given that in this example it is actually important.) (Speaking of empty: surely the empty category should count as locally cartesian closed :-) I am piling up parentheses in an effort to be social.)
About local homeomorphisms, here are three related examples that I like: polynomial functors and cartesian maps, decomposition spaces and culf maps, Petri nets and etale maps. A general class of examples are Joyal's axiomatically defined classes of etale maps [see Joyal-Moerdijk: Completeness theorem for open maps]. They always form a locally cartesian closed category, generally not with a terminal object.
Cheers, Joachim.
PS: by 'nonempty' I meant 'inhabited', of course.
_______________________________________________ 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
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
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 tocategories-list-leave@categories.org.au
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
participants (15)
-
Eduardo Dubuc -
Emily Riehl -
George Janelidze -
Henning Basold -
Joachim Kock -
Jon Sterling -
Joyal, André -
Martin Escardo -
Michael Shulman -
P.T. Johnstone -
Richard Garner -
Richard Wood -
Ross Street -
Steve Awodey -
李光熙