Update Function.Endomorphism.* to avoid use of deprecated Function.Equality

[jamesmckinna]

The #759 deprecation effort left some residues which still import (at least) Function.Equality (with a pragma to suppress the warning), notably:

• Function.Endomorphism.Setoid
• Function.Endomorphism.Propositional

which define the monoid etc. of endomorphisms (needed for a development of Foldable cf. generalising #1281 , and also now #2350 ).

UPDATED: blocked on not-yet-merged #2240 each of the above also uses the long-since-deprecated (v1.5!) Algebra.Morphism.Is*Morphism definitions instead of updating to the ones in Algebra.Morphism.Structures ...

Should update to remove dependency on the deprecated module(s).

[JacquesCarette]

Unfortunately the PR itself is regarded as a breaking change (even though not doing this for v2.0 was an oversight), so this issue should also get that label.

[jamesmckinna]

So the non-breaking suggestion on #2342 would be (instead) to introduce Function.Endo.* as new modules, and deprecate the Function.Endomorphism.* modules...?

[JacquesCarette]

Yes, I think that that name makes more sense than .New. I'll implement that.