Simplify dependencies in Codata.Musical.Colist

[jamesmckinna]

Lightened dependency on Data.Nat.Base
Removed dependency on Data.Nat.Properties

[jamesmckinna]

This arises as a knock-on effect of working on PR #1837. It's 'trivial', and removes dependencies which nevertheless reappear if you wish to consider Properties of musical colists...
... so the real reason for flagging it is to draw attention to a separate 'library design' issue: should one include 'redundant' imports in 'base' files, in order to cue the reader to their need to be imported in cognate client modules?

[MatthewDaggitt]

should one include 'redundant' imports in 'base' files, in order to cue the reader to their need to be imported in cognate client modules?

No I don't think so. We should keep the imports minimal. Otherwise you end up importing large portions of the library that you don't want. Have I got the right end of the stick?

[jamesmckinna]

@MatthewDaggitt Matthew, I agree with you (and you have the right end of this stick).

But I've noticed more than once that this ('over-importing') is a 'pattern' (not sure what to call it; a tic, perhaps) in the library... so one day we might need to do a more systematic trawl to minimise imports everywhere. But I'm reluctant to do such a systematic job, except on a case-by-case basis with each PR, as I find it hard to think about how to rationally/better/best prune the import interfaces with 'using'... and I'm not always clear what the 'rational' pruning strategy might be... because the more you name, the more knock-on viscosity you have to deal with when you you rename, etc.

[MatthewDaggitt]

But I've noticed more than once that this ('over-importing') is a 'pattern' (not sure what to call it; a tic, perhaps) in the library... so one day we might need to do a more systematic trawl to minimise imports everywhere.

Yes it's a legacy of our refactorings that don't update the imports when we shift contents out of modules. To be honest its near impossible to keep track of unused imports without editor support. One of the things that it would be great to add to the Agda language server (and put in the infrastructure grant proposal).