Add unique morphisms from/to `Initial` and `Terminal` algebras

[jamesmckinna]

Following up on #1906 , but with different location for the constructions.

• [x] Monoid
• [x] Group
• [x] NearSemiring
• [x] Semiring
• [x] Ring

PR does not introduce Algebra.Morphism.Construct.Zero, by contrast with Algebra.Construct.Zero, because the initial/terminal morphisms are different, even while the zero objects are identical...

[JacquesCarette]

I think I liked OneMorphism and ZeroMorphism (without the cuteness) more than The. In some ways, if these files are meant to be used qualified, then just Morphism might work, so that they would be Terminal.Morphism and Initial.Morphism.

[jamesmckinna]

I think I liked OneMorphism and ZeroMorphism (without the cuteness) more than The. In some ways, if these files are meant to be used qualified, then just Morphism might work, so that they would be Terminal.Morphism and Initial.Morphism.

I don't want to make this a hill on which either of us die defending... I'd be happy/ier with plain Morphism than One or Zero (I agree with removing the cuteness), but I liked the rhetorical force (not: cuteness!) of the The (Unique... would also work?).

[JacquesCarette]

Unique has a certain charm to it, I agree.

[jamesmckinna]

Happy to merge, and will try to abstain in future from my inclination towards boilerplate/bureaucracy...