Dependency of Algebra.Properties on Algebra.Bundles or Algebra.Structures? Similarly: Relation.Binary.Reasoning.*

[jamesmckinna]

At present (v2.x-v3.y transition), we make Algebra.Bundles.X the type of parameter to

• Algebra.Properties.X
• Relation.Binary.Reasoning.* (defined relative to Relation.Binary.Bundles!) for the appropriate sub-bundle of the corresponding X.

I think that this is a mistake, because it violates the (implicit?) meta-design principle that

• Structures should only depend on Structures (cf. README.Design.Hierarchies)
• Bundles can depend on Structures, Bundles, and Properties
• (unstated) that Properties should depend only on axiomatisations, ie Structures

Moreover, it seems to have forced us to plumb in a setoid (Bundle!) manifest field at the very base of Algebra.Structures in order to streamline the ergonomics of being able to do Relation.Binary.Reasoning.Setoid within structures (maybe there are no longer instances of this phenomenon, but no reason a priori to forbid it, for extensibility reasons). In like fashion to the above, the Reasoning combinators/syntax only actually depend on the IsEquivalence/IsPreorder axiomatisation, ie. the underlying Relation.Binary.Structures.IsX...

This strays uncomfortably close to hypothetical-rewrite territory, not least because it would have a lot of knock-on consequences wrt module parametrisation, but I think in the end it will be The Right Thing To Do to parameterise Properties and Reasoning (as a special kind of properties!?) on Structures.

Related issues/PRs:

• [DRY] Reconciling the indices of IsX with those of the corresponding RawX #2252
• [ discussion ] alternative design for Algebra.Structures.IsX and Algebra.Properties.X #2762
• [ design ] Re-exports from Algebra.Properties.X #2804
• each of the above referenced from my comment on #3003

I have the feeling that I, among others, have raised related issues several (many?) times in the past:

• 'wide' vs. 'narrow' Algebra.* APIs...
• ...?

[JacquesCarette]

This is the eternal "(un)bundling" discussion.

My current opinion: in the current Agda, whatever decision is made on this will be sub-optimal. We would be forcing a particular compromise which would always turn out to be uncomfortable for certain cases. Arend has shown the correct way to do this: don't choose.

[jamesmckinna]

Thanks Jacques. We've touched on this several times before, and while I would like a 'don't choose' solution, Agda's affordances seem to require us to choose... and agree on the choice! And so we need to decide which choice is 'preferable' for the ergonomics of development and use of the library, and clarity regarding downstream client uses of the library:
"If you want to work in/on Group theory, you should import the following modules:

• ...
• together with, for a given Group G within which you wish to work, a parameter/hypothesis of the form G : Group _ _
• and an opening preamble of the form private module G = Group G from which all primitive components/axioms are available
• and import Algebra.Properties.Group G as Properties from which admissible/derivable properties may be accessed
• and import Relation.Binary.Reasoning G.setoid as ≈-Reasoning in order to be able to do equational reasoning in G
  "

The main 'design' decision I see currently unimplemented, or at least, not-always-consistently implemented, is the one I identify in #2804 :

• if IsX/X defines a subsubstructure/bundle IsY/Y (possibly multiple), ...
• ... then Algebra.Properties.X should re-export (suitably renamed if necessary each of the Algebra.Properties.Y for such sub-gadgets