Enforcing the new algebra naming conventions for Algebraic Structures

[thomas-lamiaux]

I have started to enforce the algebra naming convention for algebraic structure.
I will just modify the Base.agda and fix the dependencies.
However, I will not enforce notation like Invol in the properties files that might be done in a next PR.

[thomas-lamiaux]

@felixwellen or @mortberg is there a reason for https://github.com/agda/cubical/blob/master/Cubical/Algebra/Monoid/Base.agda#L36 ?
Because IdL and IdR are beneath, and in practice one always use that and not identity.
So I don't see the point of having such constructors ?
Shouldn't we replace it by two constructors IdL and IdR ?

[kangrongji]

I guess the reason is, identity is an h-proposition. One-side unit is not unique under non-commutative multiplication.

[mortberg]

@felixwellen or @mortberg is there a reason for https://github.com/agda/cubical/blob/master/Cubical/Algebra/Monoid/Base.agda#L36 ? Because IdL and IdR are beneath, and in practice one always use that and not identity. So I don't see the point of having such constructors ? Shouldn't we replace it by two constructors IdL and IdR ?

I don't think there's any deep reason for this and it could as well be split into two fields

[thomas-lamiaux]

One-side unit is not unique under non-commutative multiplication.

I don't really understand what you mean ?
Because the way, one proved that it is a proposition is by using
isPropΣ : isProp A → ((x : A) → isProp (B x)) → isProp (Σ A B)
and so by having as in hypothesis that it is a Set then by funExt it follows.

This would be case whether it separated or not.
Actually the current proof is done by proving them separately using
(λ semi → isPropΠ λ _ → isProp× (semi .is-set _ _) (semi .is-set _ _)))

[thomas-lamiaux]

@mortberg Then should I replace it by two fields ? (and the similar ones)
Because It seems to me as adding a useless construction in the basic files.

[kangrongji]

One-side unit is not unique under non-commutative multiplication.

I don't really understand what you mean ? Because the way, one proved that it is a proposition is by using isPropΣ : isProp A → ((x : A) → isProp (B x)) → isProp (Σ A B) and so by having as in hypothesis that it is a Set then by funExt it follows.

This would be case whether it separated or not. Actually the current proof is done by proving them separately using (λ semi → isPropΠ λ _ → isProp× (semi .is-set _ _) (semi .is-set _ _)))

Oh... You're right, the ε is given as parameter.

I thought the ordinary definition of "having a unit" is Σ[ ε ∈ A ] (x · ε ≡ x) × (ε · x ≡ x), and it is h-proposition, so that one don't need ε as a constructor. But since here ε is given explicitly, it's irrelevant.

[mortberg]

@mortberg Then should I replace it by two fields ? (and the similar ones) Because It seems to me as adding a useless construction in the basic files.

Sure, sounds good

[thomas-lamiaux]

Should the following be deleted ? https://github.com/agda/cubical/blob/master/Cubical/Algebra/Group/Base.agda#L32

[mortberg]

Should the following be deleted ? https://github.com/agda/cubical/blob/master/Cubical/Algebra/Group/Base.agda#L32

Maybe not deleted, but maybe moved to abelian groups? Additive groups are usually abelian...

[thomas-lamiaux]

Yes this what I meant, this shouldn't be in Group but AbGroup

[thomas-lamiaux]

should be merge after the others PR

[thomas-lamiaux]

I have introduced nice notation for AbGroup

  open IsGroup isGroup public
    renaming
      ( ·Assoc      to +Assoc
      ; ·IdL        to +IdL
      ; ·IdR        to +IdR
      ; ·InvL       to +InvL
      ; ·InvR       to +InvR)

but then, it would also be nice to be able to do something like

pres1       to pres0
presinv    to pres-
pres·        to pres+

but I don't really know how to that as right now the definition is just calling back the definition of group

[mortberg]

I have introduced nice notation for AbGroup

  open IsGroup isGroup public
    renaming
      ( ·Assoc      to +Assoc
      ; ·IdL        to +IdL
      ; ·IdR        to +IdR
      ; ·InvL       to +InvL
      ; ·InvR       to +InvR)

but then, it would also be nice to be able to do something like

pres1       to pres0
presinv    to pres-
pres·        to pres+

but I don't really know how to that as right now the definition is just calling back the definition of group

Won't we have the same problem for pretty much all the theory about groups? If lemmas are named using the multiplicative notation then they will look ugly for the additive notation. I don't know if it matters or what we can do.

[felixwellen]

I think it does matter, since it adds to the confusion, if things don't look like they would look in math.
But I also don't know a good solution. Redefining things as records that could also just be definitionally equal (like AbGroupHom and GroupHom, CommRingHom and RingHom, ...) is also annoying.

[thomas-lamiaux]

@felixwellen I am currently fixing the dependencies.
In you PR, why did you put stuff like AbGroup->Group or makeAbGroup in a module ?
Is that to prevent it to unfold ?

If there is really some specific trick that is known hat prevent unfolding or thing like this, that really made working easier, maybe it should be mention in contributing ?
Like recommended practice to enhanced the code and computation, so people can be aware ?

[thomas-lamiaux]

@mortberg Would it be possible to merge this before others conflict are added ?
There is currently no PR that conflict it except mine but I rather fix the direct sum PR directly than fixing this one again

[mortberg]

@mortberg Would it be possible to merge this before others conflict are added ? There is currently no PR that conflict it except mine but I rather fix the direct sum PR directly than fixing this one again

Ignore my other message

[mortberg]

Looks great! Massive improvement to the Algebra package!

I found a few small things that should be fixed before we can merge

[mortberg]

Puh, no conflicts after I merged my PR about induced structures!

@felixwellen @ecavallo @mzeuner Are there any other PRs that should be merged before this one or can we go ahead and merge it once @thomas-lamiaux has fixed my comments? I hope we can merge this one very soon to avoid having any more conflicts in it...

[thomas-lamiaux]

Ha probably a bug because my branch is not up to date

[thomas-lamiaux]

The bug that broke the last check is a bit unexpected. I think that I removed some useless import.
But then someone used them to add something in an other branch and then when merging it removed them even though they were now needed.
Should be good now

[thomas-lamiaux]

@mortberg good to go

[mortberg]

No objections, so merged!