Zulip Chat Archive

Stream: maths

Topic: category/


view this post on Zulip Reid Barton (Apr 28 2020 at 23:09):

@Scott Morrison is the plan to both move the category_theory directory, and also change the namespace?

view this post on Zulip Reid Barton (Apr 29 2020 at 02:08):

Also, what's the purpose of this change exactly? Just changing the name for change's sake, so we don't have to type _theory? Or is there more to it?

view this post on Zulip Scott Morrison (Apr 29 2020 at 05:52):

My intention had been to renamed both the directory and the namespace.

view this post on Zulip Scott Morrison (Apr 29 2020 at 05:54):

I'm sorry if this seems pointless. :-( My intention had just been to reduce confusion between the category and category_theory directories, but it had not actually occurred to me to achieve this by merely renaming category to control and leaving category_theory as is. I had always thought that the name ought to be just category and wasn't because it already existed as something else.

view this post on Zulip Scott Morrison (Apr 29 2020 at 05:54):

I am perfectly happy to leave category_theory as it is now.

view this post on Zulip Reid Barton (Apr 29 2020 at 11:29):

I don't have a strong opinion about either of these renames, but I just wanted to point out that the rename wouldn't actually fix the problem where you write, say, functor.id and Lean picks the wrong one.

view this post on Zulip Scott Morrison (Apr 29 2020 at 11:38):

Yes. That I was imagining as a still later experiment, seeing how painful it would be to put functor and friends into a control namespace.

view this post on Zulip Patrick Massot (Apr 29 2020 at 12:04):

I think renaming the category folder to something else was crucial. Everything else is optional.

view this post on Zulip Patrick Massot (Apr 29 2020 at 12:04):

But consistency would be nice. We have ring_theory, field_theory but topology, algebra...

view this post on Zulip Reid Barton (Apr 29 2020 at 17:37):

I agree that having both category_theory and category was bad.


Last updated: May 14 2021 at 18:28 UTC