[ refactor ] make Relation.Binary.Morphism.Definitions obsolete

[jamesmckinna]

This tackles the first part of #2875 , retaining the module solely for compatibility per #1206 / #1213 as requested by @pnlph , so no actual deprecation at this stage.

Knock-on consequences include:

• hopefully simplifying the dependency graph wrt imports of Function.Definitions vs. alternatives
• replacing the definition Homomorphic₂ throughout by Function.Definitions.Congruent (but the name is still exported as public by the obsolete stub; and hence also exported by Relation.Binary.Morphism, but this could be removed/deprecated?)
• etc.

TL;DR: the 'cause' of the problem is yet again [ DRY ] with some basic concepts duplicated across the Function/Relation/Algebra hierarchies as various specialisations (or not even that) of 'common' (very) general abstractions (eg 'monotonicity'/'congruence'/'respects') which different authors have, at different times, identified as Core to one or other hierarchy... cf. #2917

[jamesmckinna]

NB, this too could be replaced by

Suggested change

	open import Relation.Binary.Definitions using (Monotonic₁)
	open import Function.Definitions using (Congruent)

But at the cost of straying outside the Relation.* hierarchy...

[JacquesCarette]

Since morphisms tend to be functions, using Function.Definitions where does not seem out of place.

[jamesmckinna]

Although here, as the definition is being used in a context where the monotonicity of the function is being appealed to, I think is makes slightly more sense (cognitive load? 'documentation'?) to prefer Monotonic₁ in this instance?

[jamesmckinna]

Alternatively,

Suggested change

	using (Congruent; Injective; Surjective; Bijective)
	using (Injective; Surjective; Bijective)
	renaming (Congruent to Homomorphic₂)

[JacquesCarette]

Putting as comment, since I don't want to block merge on just this.

[JacquesCarette]

Since morphisms tend to be functions, using Function.Definitions where does not seem out of place.