agda-stdlib [ refactor ] Add equality as a parameter to `Algebra.Consequences.Base`

See this comment on issue #2502 .

By analogy with Algebra.Definitions and Algebra.Structures... moreover non-breaking. Indeed, Base is only imported by Algebra.Consequences.Setoid (and by the now-deprecated module Algebra.FunctionProperties.Consequences.Core), so there should be no knock-on consequences (sic) for client modules.

Feb 06 '25 12:02 jamesmckinna

Currently this feels like two different PRs merged into one. One with a load of refactorings. One with the change to the equality parameter. Is it possible to separate them out to make them easier to understand and review?

Feb 19 '25 02:02 MatthewDaggitt

Currently this feels like two different PRs merged into one. One with a load of refactorings. One with the change to the equality parameter. Is it possible to separate them out to make them easier to understand and review?

Good, thanks @MatthewDaggitt . The 'pure' refactoring PR now split off as #2592 , on which this PR (with the change in top-level parameterisation) then blocks. After merging that (and rebasing this one against the resulting master), this should then be fine to proceed with a lower reviewing burden... I hope ;-)

Feb 19 '25 12:02 jamesmckinna

I'll return to the merge conflicts after v2.3, given that this is currently blocking on a breaking v3.0 change.

Mar 24 '25 10:03 jamesmckinna

Is it fundamental that the bulk of this is blocked on something breaking?

Jul 30 '25 20:07 JacquesCarette

Is it fundamental that the bulk of this is blocked on something breaking?

It's a while now... since I thought about this PR, and in the interests of not trying to page too much back in just now, I'm happy to leave all of these things to v3.0, given your proposed time line to start in earnest on that?

Jul 31 '25 09:07 jamesmckinna