`DirectProduct`s etc. in the `Algebra.*` hierarchy

[jamesmckinna]

Algebra.Construct.DirectProduct and Algebra.Module.Construct.DirectProduct define some objects which are the binary products of the appropriate algebras, which are moreover in some case also biproducts (products and coproducts together).

This is fine as far as it goes, but does not extend to I-ary products and sums of (at least) modules (sums have only finitely-many non-zero components, whereas products can have arbitrary I-ary functions in the carrier)

Analogously to #1906 / #1902 , suggest a refactor to put things 'in the right place':

• define Product to introduce all the product algebras;
• define Sum (or Coproduct) to introduce the coproducts;
• re-export those which are biproduct objects inDirectProduct;
• consider deprecating that module in favour of Biproduct;
• ADDED: #2244 makes explicit the left-/right injections (homomorphisms!) from the components of a binary direct sum; so these should be added as part of the construction; as should the corresponding projections for (binary) direct products... together with the injection/projection relations in the case of biproducts...

It seems easiest perhaps to begin by localising things first in Algebra.Module.Construct.* as a prototype for the the larger task in Algebra.Construct.*

[JacquesCarette]

Agda will have the best engineered library of them all! (I mean that).

[jamesmckinna]

I'll take that as encouragement!

[JacquesCarette]

That's how it was meant. What I really want to do next is to emulate (the good parts of) Kevin Buzzard and put as many students on implementing things as possible. The more ready designs we have, the faster that will go.

[jamesmckinna]

Suggest that this wait until after the v2.0 release. ;-)