Add `Algebra.Construct.WreathProduct` and/or `Algebra.Construct.SemiDirectProduct` about agda-stdlib HOT 7 OPEN

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

from agda-stdlib.

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.

from agda-stdlib.

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.

from agda-stdlib.

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!

from agda-stdlib.

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.

from agda-stdlib.

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...

from agda-stdlib.

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

UPDATED: #2381

from agda-stdlib.