search

agda / agda-stdlib

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

Add `IsIdempotentMonoid` and `IsCommutativeBand` to `Algebra.Structures` #2402

Closed jamesmckinna closed 3 weeks ago

jamesmckinna commented 4 weeks ago

UPDATED Fixes #2138 (and a bit more!)

NB: (possible downstream PRs?)

Taneb commented 3 weeks ago

I think we should change Algebra.Lattice to refer to these structures somehow

jamesmckinna commented 3 weeks ago

I think we should change Algebra.Lattice to refer to these structures somehow

Downstream PR?

Since IsSemiLattice and IsBoundedSemiLattice are already aliases for Algebra.Structures (and now may be have been replaced directly with the new definitions), is the migration path to drop in the new structures in place of those names, and correspondingly deprecate the old names?

jamesmckinna commented 3 weeks ago

Have redefined IsSemilattice and IsBoundedSemilattice as aliases for the new structures, but have not deprecated the old names (lots of knock-on viscosity elsewhere in the library).

Consider deprecation of the 'old' names as a downstream issue/PR?

UPDATED: not clear whether the redefinition needs to be recorded in the CHANGELOG... there was knock-on to do with use of the definitions, but AFAICT, the typing/parametrisation/dependency structure is preserved... welcome a review which looks closely at this! Have now added a line to the CHANGELOG ;-)

jamesmckinna commented 3 weeks ago

I'm reviewing this in a train station, so I could be wrong, but I think you're missing that a commutative idempotent monoid is a commutative band?

See comment above: L250-L251. (were you perhaps behind in the commit history?) UPDATED: ah... you meant under Bundles... d'oh!

And also IdempotentSemiring is missing... A lot of these, maybe now without be a good opportunity to add the links

Latest commit augments IsIdempotentSemiring with the relevant substructures (I hope! please check...).

Latest latest commit augments IdempotentSemiring with the relevant subbundles (I hope! please check...).

After that, I'd be tempted to say that additional (sub)structures should be downstream PRs, unless you find any glaring omissions!? (but no need to do so until after your journey's end...)