[ fix ] parametrisation of `Relation.Binary.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₂ _ _ f could be given by delegation to f Preserves _∼₁_ ⟶ _∼₂_ from Relation.Binary.Core. Indeed, that the whole module-level parametrisation could be rejigged using variables to streamline things more smoothly?

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.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.)