Zero objects in the Algebra.* hierarchy

[jamesmckinna]

Algebra.Construct.Zero defines some zero objects (magma, semiring, band) which are not zero objects, only terminal ones. Correspondingly, true zero objects defined there should also be re-exported as initial objects. Suggest a refactor to put things 'in the right place':

• define Terminal to introduce all the terminal algebras;
• re-export the subset of those which are zero objects also in Initial and Zero;
• define the true initial objects for Magma, Semigroup, Band in Initial

See PR #1902

[Taneb]

I think we should (not necessarily in the PR that closes this, but maybe) include the defining properties of these initial/terminal/zero objects, so for example for initial objects, that there is a unique homomorphism from them to any other object. Maybe this can go somewhere like Algebra.Construct.Initial.Properties?

[JacquesCarette]

1. Yes!
2. Next PR. Let's not achieve paralysis by drowning the great by requiring perfection.

[jamesmckinna]

@Taneb you're absolutely correct. I had held off pointing out the 'missing' universal constructions of the unique homomorphism, partly out of 'tact', partly out of not knowing exactly where the library designers think (and: can agree!) that such things should live (see previous discussion about Free constructions, homomorphisms...) and partly out not wishing to (re-)duplicate work which may be already present in agda-categories... but that larger project, of injecting that library into stdlib is challenging work for another day... obviously in conjunction with @JacquesCarette

Against @MatthewDaggitt 's concerns about potential deprecation of the Zeromodule, if it ends up being too 'thin'/'empty', then it might indeed be fruitful to put all the unique homomorphisms in with the various Constructions themselves.

[jamesmckinna]

Closed by #1902