[Import] Codata.*

[jmougeot]

No description provided.

[JacquesCarette]

looks good (but again, need to wait for CI)

[jamesmckinna]

See my comment on #2617 about Codata.Musical.Notation.

UPDATED: I guess after looking again at that merged PR, that I now accept, albeit reluctantly, the explicit mention of the 'musical' notation. I think that it might be useful separately, perhaps under #2339 , to discuss whether it is a good idea or not to explicit expose the API of a given import in this way, in terms of knock-on viscosity (but I take the spirit of @JacquesCarette 's intentions, and @jmougeot 's implementations in this series of PRs, to be: yes, it's worth the cost, because this is a way of seeing upfront what has to be paid, rather than having to search for it, or be taken by surprise by it, later)

[jamesmckinna]

Given all this activity in 'regularising' the role of imports with using directives, standardising the order of names mentioned (type before constructors, constructors before functions, functions before relations, or simply 'module dependency order'?) seems a good idea?

[jamesmckinna]

Time to merge!