Standardise names for qualified module imports

[jamesmckinna]

Task list to address #2201 , itemised by what needs to change (with proposed changes), rather than where (too many imports to list!):

• *.Bundles as Bundles
• *.Bundles.Raw as Raw
• *.Consequences{.*} as Consequences
• *.Construct.Composition as Composition
• *.Construct.Identity as Identity
• *.Definitions as Definitions
• *.Effectful.Transformer as Transformer
• *.Structures as Structures
• Data.Nat{.*} as ℕ Qualified import of Data.Nat fixing #2280 #2281
• Data.Integer.Divisibility: this module makes qualified imports from various Data.Nat modules, but it doesn't seem easy to import them all under a single qualified name ℕ, because the structure seems to need to export the constructor divides of Data.Nat.Divisibility, leading to a disambiguation error... perhaps this can be renegotiated/refactored via Data.Nat.Divisibility.Core introducing a pattern synonym? Qualified imports in Data.Integer.Divisibility fixing #2280 #2294
• Data.Product.Base as Product (or Σ?) Qualified import of Data.Product.Base fixing #2280 #2284 NB Data.Container.* yields non-trivial ambiguities
• Data.Sum.Base as Sum (or ⊎?) Qualified import of Data.Sum.Base fixing #2280 #2290 NB Data.Container.* yields non-trivial ambiguities
• Data.X.Properties as X, rather than Xₚ with X the datatype name, not the ASCII module name (as in ℕ above) Qualified import of Properties modules fixing #2280 #2283 NB see the caveats on that PR
• Function.* as Function
• Relation.Binary.PropositionalEquality{.*} Qualified import of PropositionalEquality etc. fixing #2280 #2293 (systematic but terrifyingly pointless)
• Relation.Binary.Reasoning.Setoid as ≈-Reasoning by analogy with ≡-Reasoning Qualified import of reasoning modules fixing #2280 #2282 / Style guide: guideline for -Reasoning module imports cf #2282 #2309
• Relation.Binary.* as Binary
• Relation.Nullary.* as Nullary (exceptions for Decidable and Negation?)
• Relation.Unary.* as Unary
• README.* Tidy up README imports #2280 #2313
• ...

TODO: update style-guide to incorporate the conventions:

• final choices of names for Sum and Product
• ...

Things to leave alone:

• Foreign.*
• System.*
• ...

Design decisions/outstanding questions:

• use of Unicode: we had agreed in What names should be used for qualified module imports? #2201 to the use of ℕ as the qualified module name for the (most-?) common cases of importing qualified from Data.Nat.*, and equality as ≡ from Relation.Binary.PropositionalEquality.*; but as the list above asks: what about the qualified import names for Sum and Product?
• what to do where the style guide recommendations cannot be followed?

NB. Each of the above tasks/associated PRs seems to have one or two 'leftovers', so a final 'mop-up' PR may well be in order once the above list (or a suitable subset) is completed.

[jamesmckinna]

On #2284 @JacquesCarette wrote:

Sigh - Product is non-trivially longer than Prod. But this is the right thing to do.

So... I've been reconsidering this, and wondered if, instead, and in line with the 'datatype name as root module name' heuristic, that we standardise on import Data.Product.Base as Σ?

Originally posted by @jamesmckinna in #2284 (comment)

Single precedent in stdlib: Data.Vec.Functional.Relation.Unary.Any!

[JacquesCarette]

And as I said on #2284 , I think that's a reasonable suggestion. (I'm still torn because my math background wants me to see Σ as a sum, and I can't be the only one. But that ship has sailed a long time ago, so I'm definitely not going to re-litigate that.)

[jamesmckinna]

Re: #2284 I think the maintainers should all agree on this, and then revert that PR in favour of the new suggestion, if necessary.