Zulip Chat Archive

Stream: maths

Topic: category_theory.category_struct.comp arguments


view this post on Zulip 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.

view this post on Zulip Keeley Hoek (Jun 11 2019 at 02:44):

I don't think that there's an obstruction to either interpretation.

view this post on Zulip Johan Commelin (Jun 11 2019 at 05:10):

@Yury G. Kudryashov Welcome on the chat!

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 11 2019 at 05:11):

The opinions are maybe somewhat divided...

view this post on Zulip Johan Commelin (Jun 11 2019 at 05:12):

One (not entirely satisfactory) solution is to locally provide a notation for "normal" composition order.

view this post on Zulip 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.

view this post on Zulip Reid Barton (Jun 11 2019 at 10:30):

Oh, is the End has_mul instance also backwards?

view this post on Zulip Reid Barton (Jun 11 2019 at 10:31):

I never noticed that. Yeah, I definitely think we should fix that one

view this post on Zulip Yury G. Kudryashov (Jun 11 2019 at 10:32):

I can submit a PR in a day or two.

view this post on Zulip Reid Barton (Jun 11 2019 at 10:33):

You might find that it also affects category.fold ... hopefully not too much of a mess.

view this post on Zulip Reid Barton (Jun 11 2019 at 10:33):

I think it should just be a matter of switching the definitions of foldl and foldr

view this post on Zulip 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".

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 10:36):

[way -> why] :-)

view this post on Zulip Yury G. Kudryashov (Jun 12 2019 at 02:29):

Submitted #1128

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Jun 18 2019 at 13:05):

Sorry, I've been meaning to get back to it. I'll have a look today

view this post on Zulip Yury G. Kudryashov (Jun 18 2019 at 20:27):

@Simon Hudon @Johan Commelin Sorry, I tagged a wrong person first on github, then here.

view this post on Zulip Johan Commelin (Jun 27 2019 at 05:55):

@Simon Hudon Do you have time to take a look at this?

view this post on Zulip Simon Hudon (Jun 27 2019 at 13:55):

Yes, I'll have a look now. Sorry for taking so long

view this post on Zulip 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: May 14 2021 at 19:21 UTC