[Agda] Algebra.Morphism question

[Chris Casinghino]

Hello again, fellow Agda hackers.

In the standard library, Algebra.Morphism gives a definition of ring
homomorphisms.  I was surprised to see no requirement that the
transformation preserve the rings' equality - something like:

    ⟦_⟧-preserves-≈ : ⟦_⟧ Preserves (_≈_ From) ⟶ (_≈_ To)

in the _-RawRing⟶_ record.

Should this be added, or is there a reason to admit functions which
don't respect ≈ here?  I confess I am completely new to reasoning
about algebra in agda, and the ≈ parameter had me a little confused at
first (perhaps still).

Thanks!

--Chris Casinghino