Useless import and make

[thomas-lamiaux]

When cleaning the code, I have realized that there is actually a lot of files that import module that are not used at all. This annoying because when renaming or moving something, this can create a lot of dependencies.

A make like during the compilation of the pull request, should check if the agda files are importing useless modules. An automatic method would enable to clean considerably the code and ensure that people are no longer importing anything.

[MatthiasHu]

I tried to search for unused imports recently: https://github.com/agda/cubical/pull/732 . I got the impression that there is currently no good automatic way of doing this.

I tried this tool, but it doesn't support all agda features, so the best I could think of was running it on individual files instead of the whole library and ignoring all the cases where it failed.

[thomas-lamiaux]

As it can be seen in #824 for instance https://github.com/agda/cubical/pull/824/files#diff-4a2a2c1432b474e7043879a7522d65805ad61112d16267e130091b89d4ee29b1L7, there is still a lot of useless import that can be removed.