[ fix ] parametrisation of `Algebra.Consequences.Base`

[jamesmckinna]

(Pulling on a loose thread spotted while working on #2881 )

Currently, this module at the top-level is parametrised only by the underlying Carrier telescope {a} {A : Set a}, while its local submodules then take an ambient ('raw') 'equality' relation as an explicit parameter after (the equivalent of) the various RawMagma etc. operations given implicitly.

A breaking (sigh) change would instead be to make the top-level parametrisation wrt (the equivalent of) the RawSetoid a ℓ, ie. {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) (as with Algebra.Definitions and Algebra.Structures), and only then parametrise the local submodules wrt the operations concerned. cf. #2572

Consequences:

• conceptual: equality comes before any of the rest of any algebraic signature
• consistency with Algebra.Definitions and Algebra.Structures
• pragmatic: implicit operation bindings could then be lifted out as variable declarations cf. [ refactor ] use variables in Algebra.Consequences.Base #2592
• DRY:
  • Algebra.Definitions could be opened once and for all instantiated at _≈_ in Base
  • qualified import of Base in Algebra.Consequences.Setoid could then be opened once and for all instantiated at _≈_
  • the need for the odd use of hiding gymnastics in [ bug/refactor ] put Algebra.Consequence.Propositional.sel⇒idem in the right place  #2881 is avoided
• ...?

It's (slightly) hard to see how bad the knock-on effects would be for users, but it definitely would rearrange ordering within any explicit binding telescopes at call-/use-sites, so a breaking change, but definitely worth doing for v3.0, I think!

[jamesmckinna]

Closing as (yet another) variation on #2502 ... and the associated PRs now mentioned above ;-)