[ fix ] parametrisation of `Relation.Binary.Morphism.Definitions` and `Algebra.Morphism.Definitions`

[jamesmckinna]

In the first case:

• the top-level module parameters bind A : Set a and B : Set b explicitly
• and then defines Homomorphic₂ taking explicit arguments (_∼₁_ : Rel A ℓ₁) and (_∼₂_ : Rel B ℓ₂)

It seems 'obvious' that A and B could be given implicitly instead (but: breaking!), moreover that Homomorphic₂ could be given by delegation to f Preserves _∼₁_ ⟶ _∼₂_ from Relation.Binary.Core UPDATED Function.Definitions.Congruent.

Indeed, that the whole module-level parametrisation could be rejigged using variables to streamline things more smoothly? module could be left as a stub, purely for compatibility cf. #1206 / #1213 . UPDATED: see #2922

In the second case:

• the top-level module parameters bind A : Set a and B : Set b explicitly, together with (_∼₂_ : Rel B ℓ₂)
• and then defines Homomorphic₂ taking explicit argument (f : A → B) (and the binary operations)

It seems 'obvious' here that B at least could be given implicitly instead (but: breaking!).

Are these 'bugs'/design decisions worth fixing?

Consequences:

• harmless within stdlib in the deployment contexts for Algebra.Morphism.Definitions (but: knock-ons need fixing!)
• possibly more radical for Relation.Binary.Morphism.Definitions but could be an improvement (avoid supplying 'bogus' explicit arguments A, B anywhere on qualified instantiated import...?)

[JacquesCarette]

I would be curious as to the scale of the knock-ons. For both. These are certainly excellent questions to ask. I can't help but think that, in practice, this won't be a 100% win -- but that's just a gut feel! (Trivial relations from which you can't figure out the actual carrier come to mind as times you might need to be specific. But it sure might be a 99% win.)

[jamesmckinna]

So the curiosity seems to be:

• don't bother 'fixing' the Algebra.Morphism.Definitions (hardly worth the effort)?
• whereas Relation.Binary.Morphism.Definitions can be eliminated (not-quite) entirely! [ refactor ] make Relation.Binary.Morphism.Definitions obsolete #2922