category/

Stream: maths

[Reid Barton]

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

[Reid Barton]

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]

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

[Scott Morrison]

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]

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

[Reid Barton]

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]

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]

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

[Patrick Massot]

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

[Reid Barton]

I agree that having both category_theory and category was bad.