Stream: maths

Topic: category/

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?

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?

Scott Morrison (Apr 29 2020 at 05:52):

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

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.

Scott Morrison (Apr 29 2020 at 05:54):

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

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.

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.

Patrick Massot (Apr 29 2020 at 12:04):

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

Patrick Massot (Apr 29 2020 at 12:04):

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

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