Problem with reexport items related to a Raw-structure

[mechvel]

trafficstars

This is on lib-1.7. Having M : Magma, and needing to use the divisibility _∣_, one needs to import Algebra.Properties.Magma.Divisibility. To use other items of Magma, one will be forced to import modules like Algebra.Operations.Foo. This organization of importing the items related to Magma (or any other bundle) is a bit misleading, it is difficult do guess where to search an item related to a bundle Foo.

May be it worth to add the "Reexport" modules module Foo-reexport or may be module Foo-items or module Foo-theory ? This is to reexport the items related to a bundle Foo, where these items are scattered around in Algebra.Definitions, Algebra.Properties, Algebra.Operations, and such. Personally, I am satisfied with having my home-made "Of"-modules, also I add there the user items in addition to the reexport. But the "Foo-reexport" modules in standard could make the feature easier for all users.

This looks as backwards compatible. Am I missing something?

[MatthewDaggitt]

Yes, so the properties about each individual operation are under Algebra.Properties.X as you've discovered.

To use other items of Magma, one will be forced to import modules like Algebra.Operations.Foo.

The Algebra.Operations folder is entirely deprecated. Nothing in here should be imported.

May be it worth to add the "Reexport" modules module Foo-reexport or may be module Foo-items or module Foo-theory ?

Hmm I have no problem with this, but I'm afraid I don't understand your naming convention at all. Could you elaborate on what you mean by Foo-reexport? We don't use - in names nor lowercase letters.

[mechvel]

The Algebra.Operations folder is entirely deprecated.

This is nice.

Could you elaborate on what you mean by Foo-reexport? We don't use - in names nor lowercase letters.

For example: a user has M : Monoid. One knows that in a monoid divisibility is reflexive. Also one knows that for a monoid it should be defined the function _^_ for powering, because it is easily expressed via _∙_. So the user tries to import these items from somewhere.

1. They are not exported by the Monoid bundle,
2. one has to guess that ∣-refl is in Algebra.Properties.Monoid.Divisibility,
3. one has to guess that this _^_ is in Algebra.Properties.Monoid.Foo? -- I do not know where does it currently reside, but may be it is somewhere, if not then it has to be introduced somewhere as related to Monoid.

I suggest to introduce the module Algebra.OfMonoid parameterized by (M : Monoid) which reexports all the items from Monoid, from Algebra.Properties.Monoid.Divisibility, from Algebra.Properties.Monoid.Foo?, and so on. With this, the user would not search among subfolders of the Algebra folder. Instead one would write, for example,

open Algebra.OfMonoid M using ( _∙_;  _^_; _∣_ ; ∣-refl)   

Because it is known traditionally from theory that these items are related to Monoid, and one does not need to search through various subfolders. Here _∣_ has to be reexported from OfMagma, where OfMagma to be introduced earlier similarly as OfMonoid.

Similarly, OfSemigroup and OfGroup are needed, and so on. This will add the following files to the Algebra/ folder: OfMagma.agda, OfSemigroup.agda, OfMonoid.agda, OfGroup.agda, OfSemiring.agds, and so on.

I expect this will make it easier to search for import. And this is backwards compatible. ?