Algebra.Morphism.Structures: redundant fields in ring-like morphisms

[Taneb]

Consider the IsRingHomomorphism structure. It winds up having two different, not-necessarily-equal definitions of IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧, one via the proof that addition is a group homomorphism and one via the proof that multiplication is a monoid homomorphism.

I'm working on a fix for this that defines, for example, a ring homomorphism as a semiring homomorphism plus a proof that negation is homomorphic.

[MatthewDaggitt]

Thanks, sounds like a good idea!