Refactor Algebra.Consequences.*?

[jamesmckinna]

These modules are structured around:

• Base, depending only on the underlying Carrier set A, whose properties make explicit a dependency on a(n equality) relation _≈_ : Rel A ℓ;
• Setoid, depending on a Setoid, giving rise to a relation as in Base, but with the IsEquivalence/Reasoning properties in scope;
• Propositional, essential being Setoid instantiated to Relation.Binary.PropositionalEquality.Properties.setoid A

and are used in various places to augment the signature of both specific Algebra.Structures (esp. IsGroup, Is*Ring*), and also various Algebra.Construct.*.

@Taneb 's recent #2499 draws attention to the fact that this organisation privileges Bundled Setoids over their underlying Relation.Binary.Structures.IsEquivalence fields... and thus violates the (implicit) dependency restriction of Structures only on other Structures, and not on Bundles...

So: as a hypothetical-rewrite or v3.0 refactoring, we should (perhaps!?) consider refactoring to ... sort this out. Discussion welcome!

UPDATED: similarly, the Relation.Binary.Reasoning modules depend on the underlying Bundle, and then delegate to the associated Structure via imports of lower-level Single and Double modules... and hence impacts Algebra.Consequences, via importing Relation.Binary.Reasoning.Setoid etc. so to really unpick the dependencies might involve a larger scale refactoring?

Similarly, Algebra.Properties.* depend on the associated Bundle (which seems reasonable?), and drawing clear lines between Consequences and Properties seems to be a design choice for which... the issues aren't entirely clear?

[jamesmckinna]

On further investigation:

• the admissible properties Algebra.Structure.IsGroup.uniqueˡ-⁻¹ and Algebra.Structure.IsGroup.uniqueʳ-⁻¹, which depend on Algebra.Consequences.Setoid (and hence on a public export of setoid), can de deprecated in favour of Algebra.Properties.Group.inverseˡ-unique and Algebra.Properties.Group.inverseʳ-unique respectively, where the Setoid sub-bundle is already in scope; (so: perhaps/probably should be?) see [ refactor ] deprecate Algebra.Structures.IsGroup.{uniqueˡ-⁻¹|uniqueʳ-⁻¹} #2571
• either way, those properties are nowhere used except to be (renamed and) re-exported by the IsAbelianGroup substructures in Algebra.Module.Structures, so presumably those re-exports can be handled by refactoring/reorganising in like fashion via Algebra.Module.Properties.*?
• moreover, the properties are never actually used, except (!!!) in deprecated definitions under Algebra.Morphism, specifically those which exhibit that it suffices to define a IsGroupHomomorphism via a single IsMonoidHomomorphism field, because the inverse homomorphism property is admissible... which surely should either be refactored as a Biased smart constructor, or else, now that homomorphisms are defined relative to the underlying Raw bundles... set aside entirely (cf. the discussion of admissible properties in Add bundled homomorphisms #2383 ...)
• UPDATED: they are used in Algebra.Module.Morphism.ModuleHomomorphism, but in a context where the underlying Setoid/AbelianGroup/... Bundles are in scope, and hence can be delegated to Algebra.Properties.Group instead... I think. see above.

So it looks as though the v1.5-and-after refactoring of Algebra.Structures and Algebra.Bundles still has some loose ends to tidy up. Sigh.

[MatthewDaggitt]

Yup all this analysis sounds sensible. When I first created the Consequences modules many years ago, I just needed a place to stuff this common stuff that didn't depend on the bundles in the hierarchy in question. I wasn't thinking about the long term design.

[jamesmckinna]

Badging this now as v3.0, as forming part of perhaps other, larger-scale breaking refactorings of the hierarchy.

[JacquesCarette]

It's rather fun to be seeing better design(s) emerge like this.

[jamesmckinna]

Work on #2563 suggests, at the very least, that these modules be refactored to change the (top-level) parameterisation of Base to include the equality relation, and to make the various implicit module parameters (arising from the contents of Raw signatures) global variables instead of their current, less robust/more fragile, forms... and that such a minimal intervention would not be breaking, so could be merged for v2.3... see #2572