[ refactor ] biased constructors for `Algebra.Morphism.*` etc.

[jamesmckinna]

Elsewhere, I have echoing on my mind an observation made somewhere else in GitHub (how to find such things!?) that the Group case can be further streamlined by observing something like (is this true? scratches head for a moment): any MonoidHomomorphism between (the underlying Monoid) Groups must, in fact, be a GroupHomomorphism, also by a 'cancellability' argument...?

Originally posted by @jamesmckinna in #2885 (comment)

Because: for h : G → H a Monoid homomorphism between (underlying monoids of)Groups G, H:

• h (g G.⁻¹) H.∙ h (g) H.≈ h (G.ε) H.≈ H.ε, by the hom properties
• so h (g G.⁻¹) is a left H-inverse for h (g), so by uniqueness Algebra.Properties.Group.inverseˡ-unique, they are equal.

UPDATED (I always forget that IsXHomomorphism is defined between Raw bundles!): we should add

• a lemma encapsulating the above
• but where should such a thing live?

Presumably: other such simplifications should also be possible, as we move up the Algebra hierarchy!?