For example, the functions in Naturals.agda leak out and are used pretty extensively in Integers.agda. We'd prefer to be stricter about accessing these functions in a canonical way through the appropriate group structure or whatever. A good example of this being done properly is with Orders: most uses of orders are through the well-known functions PartialOrder.irreflexive and friends, rather than specific functions like aLessA (which specifically works on the naturals only).
This is happening slowly; need to try and remove references to things which aren't Numbers.Naturals.Naturals, for example, since that module hides many of the internals of the Numbers.Naturals namespace.
For example, the functions in Naturals.agda leak out and are used pretty extensively in Integers.agda. We'd prefer to be stricter about accessing these functions in a canonical way through the appropriate group structure or whatever. A good example of this being done properly is with Orders: most uses of orders are through the well-known functions
PartialOrder.irreflexive
and friends, rather than specific functions likeaLessA
(which specifically works on the naturals only).