agda
Add `Algebra.Action.*`
~~The first is~~ This seems clear, although I wonder a bit about how best we should add Actions to the Algebra hierarchy, so going via Construct seems the best... for now (as opposed to a parallel hierarchy of 'things-acted-upon-by-things').
~~The second follows on, but is complicated by the plethora of various definitions in the literature (according to the 'thinginess' involved), and the relationship with 'semi-direct product's... so perhaps some discussion/downstream refactoring may be necessary.~~
PR incoming in the next few days, I think: UPDATED see #2350
I definitely think we're going to need either Algebra.Action or a different hierarchy altogether for multisorted Algebra. I rather think we should strongly embrace multi-sorted, rather than trying to fit it in an ad hoc way into our singly-sorted current version.
It could be argued that Algebra.* should be the home for multi-sorted. It currently isn't - but that could be a reasonable evolution.
Hmmm... I think I agree, but I'm weighing up v2.1 vs v3.0... and would like something now... with a multisorted refactoring downstream?
Well, as with Module (two-sorted: the Ring algebra acts on the AbelianGroup...), here there are two underlying carriers ('sorts' in the language of universal algebra, with sorts mapping to these distinct carriers in the construction of interpretations/models; but in general possible many, so 'multi-'), equality relations and operations going on: that of the thing acting (eg Monoid) and that of the thing acted upon (eg Setoid), with the action map relating the two...
And by "multisorted refactoring" I meant a refactoring of something I propose adding now to the vanilla Algebra hierarchy, in favour of putting it 'in the right place' in a refactored Algebra hierarchy that admits multi-sorted theories (at least that's how I understand @JacquesCarette 's suggestion...)
Right. I don't know that we necessarily need a big refactor to do this. I personally would be fine if Algebra became to mean single-sorted algebra and the multi-sorted version lived elsewhere, at least in general. Module is indeed a problem, as it is both natively two-sorted and seems to want to belong close to traditional Algebra 'modules'.
I don't think it's a great idea to go for extreme generality as a matter of principle: no one will be able to find anything. I'm a big fan of libraries that have a highly redundant user-facing 'interface'. [Implementation does not have to be redundant in that same way, for the sanity of the maintainers.]
I'd be just as fine if Algebra became the home of multi-sorted as well as single-sorted. We just need to make some kind of active decision.
Refactoring this issue to break up the two parts. What I thought would be straightforward about Wreath products seems to require more infrastructure than I am able to find already existing at the moment... esp. wrt 'pointwise' IsX structure inherited on function spaces between Setoids and other kinds X of bundle... See #2351 for the follow-on.
Meanwhile, hope you're happy @JacquesCarette with my continuing with #2350 under Algebra.Construct ahead of any decision about where such stuff should eventually end up...?
Specifically, I'm happy to entertain a v2.1 version ahead of any (eventual) active decision about Algebra.Action (which I'm warming to, but not clear I have enough bandwidth for the variety of all such things) for v3.0 (as with several other recent issues/PRs... ;-))
I certainly don't mind if a Draft PR, to shake things out, is built "in the wrong place" for parts of its contents.
See the extensive refactoring now on #2350 plus revised title for this issue... ... now reinstated as DRAFT while I reconsider some of the detailed design discussion there, but perhaps we could/should have litigated those issues here first?