Add `Algebra.Construct.WreathProduct` and/or `Algebra.Construct.SemiDirectProduct`

[jamesmckinna]

This fell originally under #2348 but I think should be factored out on its own.

Current issues:

• where is the (binary) product of Setoids defined? (plus currying etc.: cartesian-closedness of Setoid?)
• where is the (pointwise) function space from a Setoid to an algebraic structure/bundle defined, and its properties established?
• which to add first: Wreath (my preferred target) or SemiDirect?
• my interest is in the wreath product of a Monoid with a MonoidAction (#2348 / #2350 ), but many kinds of variants exist according to how much structure is present. How/where to accommodate them all?

Re: the last point. previously I wrote on #2348 as follows: (This, viz. adding wreath products, as an instance of combining 'things-acted-upon-by-things') "... 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. "

[Taneb]

The binary product of Setoids is in Data.Product.Relation.Binary.Pointwise.NonDependent: https://agda.github.io/agda-stdlib/master/Data.Product.Relation.Binary.Pointwise.NonDependent.html#7308. I don't know if we already have currying defined for setoids of the top of my head.

[jamesmckinna]

Thanks @Taneb ! I'd just about managed to find that for myself while working on #2348 / #2350 but... not the first place I might have looked for it!

[JacquesCarette]

A known, thorny issue: finding things in stdlib is very hard.

[JacquesCarette]

As I said on #2348 : it makes sense for the constructions to be in Construct but the definitions of the structure shouldn't be in the same place.

Will Wreath be a construction (only) or will it need new structures? I don't have a strong opinion on Wreath vs SemiDirect.

[jamesmckinna]

Well, again, all good questions! I think that as a construction, I should at least also need Algebra.Construct.Pointwise which does not at present exist, AFAICT. (And that is a construction... not a definition).

As for WreathProduct itself, I think that that is also a construction: given a monoid, a monoid action, then ... such and such setoid ... also admits a monoid structure...

[JacquesCarette]

Good, I think this is converging to a design: indeed WreathProduct is a construction and so Construct is a great home for it. Yes, having a pointwise product construction would also be good. Whoever needs it first can build it.

[jamesmckinna]

And yes: Construct.Pointwise (properly, should we say: Power and Copower?) should, in turn, be factored out as a distinct issue/PR!

UPDATED: #2381