agda / agda-stdlib

The Agda standard library

https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary

Other

561 stars 234 forks source link

Add bundled homomorphisms #2383

Open jamesmckinna opened 1 month ago

jamesmckinna commented 1 month ago

Cherry-picked and enhanced from #1962 . Fixes #1960 .

TODO:

[x] the Algebra.Morphism.Construct.{Identity|Composition} material
[x] RingWithoutOne doesn't appear to export its own Raw substructure, so that should be added? ditto. KleeneAlgebra
[x] homomorphisms for all the existing Structures/Bundles

doesn't address the Setoid structure on Homs at all... (brain-fade; sigh)
for bundles which export two sub-bundles, usual 'diamond' problem about re-opening those publicly for export, so someone with a good eye for such things,... please nitpick those details!
UPDATED: Semiring and Ring homomorphisms should export a SuccessorSetHomomorphism structure/bundle only after going back to #1363 through the medium of (the initial) SuccessorSet and its consequences for Algebra.Structures having (Is)SuccessorSet fields...

Taneb commented 1 month ago

Before I look at this at all I just want to say thanks for tackling it! I've been avoiding it with the hope that we can get a solution for #2287, but that looks a long way off.

jamesmckinna commented 1 month ago

@Taneb Indeed! This kind of boilerplate-bashing is quite fatiguing, until you run up against the 'diamond' re-export problem, at which point my powers fail me in different ways, trying to work out what should get re-exported from where... plus discovering that (still!) not everything is present which perhaps ought to be... ;-)

UPDATED: moving to DRAFT until I have time to finish off (some of) the outstanding items above.

jamesmckinna commented 1 month ago

@JacquesCarette @Taneb I have now added the 'missing' parts of the PR (as in the revised opening preamble above), and so (hopefully) now stopping there...

jamesmckinna commented 1 month ago

As expected, this massively screams for meta-programming. In the meantime, this is great.

2287 : yes please!

jamesmckinna commented 1 month ago

So I think that I now have added all the relevant (requested!) sub-{structure|bundle}s, but definitely needs another pass to check, along perhaps with a downstream issue/PR to fill in yet more gaps (including in the Raw sub-hierarchy, cf. #2255 ).

jamesmckinna commented 1 month ago

Thanks @JacquesCarette ! (modulo the need for manual effort in the absence of a Drasil-based solution...)

jamesmckinna commented 2 weeks ago

Currently badged as v2.2, but could merge for v2.1?