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
• [x] Data.Nat{.*} as ℕ #2281
• [x] 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? #2294
• [x] Data.Product.Base as Product (or Σ?) #2284 NB Data.Container.* yields non-trivial ambiguities
• [x] Data.Sum.Base as Sum (or ⊎?) #2290 NB Data.Container.* yields non-trivial ambiguities
• [x] Data.X.Properties as X, rather than Xₚ with X the datatype name, not the ASCII module name (as in ℕ above) #2283 NB see the caveats on that PR
• [ ] Function.* as Function
• [x] Relation.Binary.PropositionalEquality{.*} #2293 (systematic but terrifyingly pointless)
• [x] Relation.Binary.Reasoning.Setoid as ≈-Reasoning by analogy with ≡-Reasoning #2282 / #2309
• [ ] Relation.Binary.* as Binary
• [ ] Relation.Nullary.* as Nullary (exceptions for Decidable and Negation?)
• [ ] Relation.Unary.* as Unary
• [x] README.* #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 #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 https://github.com/agda/agda-stdlib/issues/2284#issuecomment-1937722328

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.