Zulip Chat Archive
Stream: maths
Topic: category_theory.category_struct.comp arguments
Yury G. Kudryashov (Jun 11 2019 at 02:34):
Hi! What is the reason to have the arguments of category_struct.comp reversed compared to function.comp? This way, e.g., an action is a homomorphism to (End β)ᵒᵖ instead of (End β), equiv.perm α is (Aut α)ᵒᵖ etc.
Keeley Hoek (Jun 11 2019 at 02:44):
I don't think that there's an obstruction to either interpretation.
Johan Commelin (Jun 11 2019 at 05:10):
@Yury G. Kudryashov Welcome on the chat!
Johan Commelin (Jun 11 2019 at 05:10):
Here is a thread with more discussion about composition order: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Convention.20on.20composition.20order/near/165699204
Johan Commelin (Jun 11 2019 at 05:11):
The opinions are maybe somewhat divided...
Johan Commelin (Jun 11 2019 at 05:12):
One (not entirely satisfactory) solution is to locally provide a notation for "normal" composition order.
Yury G. Kudryashov (Jun 11 2019 at 10:30):
@Johan Commelin Thank you for the link! I don't care about notation; I care about has_mul instance.
Reid Barton (Jun 11 2019 at 10:30):
Oh, is the End has_mul instance also backwards?
Reid Barton (Jun 11 2019 at 10:31):
I never noticed that. Yeah, I definitely think we should fix that one
Yury G. Kudryashov (Jun 11 2019 at 10:32):
I can submit a PR in a day or two.
Reid Barton (Jun 11 2019 at 10:33):
You might find that it also affects category.fold ... hopefully not too much of a mess.
Reid Barton (Jun 11 2019 at 10:33):
I think it should just be a matter of switching the definitions of foldl and foldr
Yury G. Kudryashov (Jun 11 2019 at 10:35):
That's why "a day or two", not "a few minutes after driving my kid to the day care".
Kevin Buzzard (Jun 11 2019 at 10:36):
[way -> why] :-)
Yury G. Kudryashov (Jun 12 2019 at 02:29):
Submitted #1128
Yury G. Kudryashov (Jun 18 2019 at 12:45):
Hi @Johan Commelin , could you please tell me what's wrong with the new proofs in #1128? Then I'll try to improve them myself.
Johan Commelin (Jun 18 2019 at 12:47):
@Yury G. Kudryashov I'm really not an expert on Kleisly and fold etc... I think @Simon Hudon is the person to ask.
Johan Commelin (Jun 18 2019 at 12:48):
Most of it looks fine to me. The only thing that worries me is the .get that were not there before.
Yury G. Kudryashov (Jun 18 2019 at 12:52):
There was a .get (an alias for unop) for one of foldl/foldr, and it migrated from one proofs to others. Also, I added .get to both (as aliases to id and unop) to have a common interface to foldl/foldr. Should I remove the get=id part?
Johan Commelin (Jun 18 2019 at 12:53):
@Simon Hudon :up: you know much better how you would like this part of the library to behave.
Simon Hudon (Jun 18 2019 at 13:05):
Sorry, I've been meaning to get back to it. I'll have a look today
Yury G. Kudryashov (Jun 18 2019 at 20:27):
@Simon Hudon @Johan Commelin Sorry, I tagged a wrong person first on github, then here.
Johan Commelin (Jun 27 2019 at 05:55):
@Simon Hudon Do you have time to take a look at this?
Simon Hudon (Jun 27 2019 at 13:55):
Yes, I'll have a look now. Sorry for taking so long
Simon Hudon (Jun 27 2019 at 18:23):
I made a PR on top of the PR. It's ready to merge if it works for you @Johan Commelin and @Yury G. Kudryashov
Last updated: Dec 20 2023 at 11:08 UTC