search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
570 stars 233 forks source link

Add `Algebra.Definitions.RawGroup` and `Algebra.Properties.Group.*` #2454

Open jamesmckinna opened 1 month ago

jamesmckinna commented 1 month ago

On the model of

Introducing the 'obvious' action(s) of type ℤ → Carrier → Carrier.

Plus: additional properties in the AbelianGroup case...

JacquesCarette commented 3 weeks ago

Should it really be for ℤ or for any structure that has FOO properties?

Taneb commented 2 weeks ago

@JacquesCarette what do you mean by "FOO properties"?

jamesmckinna commented 2 weeks ago

@JacquesCarette Yes, I agree, but as with the Nat action (by multiplication) for (Raw)Monoid, it first seems superficially tied to the action of the free FOO (if I understand that usage correctly).

But then we should go back and refactor the Nat (and Bool) Semiring actions for monoids. What's the best evolutionary path to follow? A mega PR doing things 'right', or else piecemeal, as in the current proposal?

And: let's agree a design for Free things, so that Nat as the free Semiring, and Z as the free Ring, on no generators, can be characterised as such... #1962 The more I pull on these threads... the more unravels!

JacquesCarette commented 2 weeks ago

@Taneb I meant it as a placeholder variable for something like Semiring, or whatever structure+property bundle is necessary to meaningfully define the concept.

Re: evolution. I'm starting to wonder if we need a companion library that builds on top of stdlib but has no strong compatibility guarantees, so that it may evolve much faster. For stdlib: I think mega PRs are very dangerous; then tend to go stale and never land. So I prefer piecemeal, so that progress actually happens. The problem with that is that mistakes might creep in to 'piecemeal' only to be discovered just-too-late. Thus my thoughts about a more experimental on-top library.

Yes, a design for Free things is likely timely.

I don't see it so much as 'threads unraveling' as (re)discovering that mathematics is internally very structured. (We're not the only ones, Rocq and Lean people are (re)discovering the same, but not necessarily in the same spots.)

jamesmckinna commented 2 weeks ago

@JacquesCarette Lots of food-for-thought in your last comments... hypothetical-rewrite redux? And as to "mathematics is internally very structured"... yes, the various modern experiments with libraries seem to recapitulate, in yet-further new ways, that there is no single, 'best', Bourbachiste solution, in spite of our more illustrious forebears in this regard?