## 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".

[way -> why] :-)

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: May 14 2021 at 19:21 UTC