Clean up: Remove Foundation/Everything and outdated stuff

[felixwellen]

No description provided.

[felixwellen]

Discussed with anders already -> merging.

[ncfavier]

What's the replacement for Cubical.{Core,Foundations}.Everything? The generated files only have import, not open import.

[mortberg]

What's the replacement for Cubical.{Core,Foundations}.Everything? The generated files only have import, not open import.

I think the idea is just to write the imports one needs instead of relying on the Everything files

[foxyseta]

What's the replacement for Cubical.{Core,Foundations}.Everything? The generated files only have import, not open import.

I think the idea is just to write the imports one needs instead of relying on the Everything files

Shouldn't https://agda.readthedocs.io/en/latest/language/cubical.html be updated then? It is still using Everything

[foxyseta]

Or maybe not since there has been no release of cubical since this PR was merged in May.

[felixwellen]

I think we could also change how the Everything-files are generated. In principle in makes sense to me, to just import everything (or a reasonable selection). I don't like the amount of imports we have in some files. It might also make sense to have something called "Common.agda" which has open imports for all the things that are usually used from some directory. Do you see any problems with that, @mortberg ?

[mortberg]

I think we could also change how the Everything-files are generated. In principle in makes sense to me, to just import everything (or a reasonable selection). I don't like the amount of imports we have in some files. It might also make sense to have something called "Common.agda" which has open imports for all the things that are usually used from some directory. Do you see any problems with that, @mortberg ?

Isn't it better to have lots of imports to speed up compilation? (More things can be done in parallel with a more specific dependency tree)

[felixwellen]

I don't know, but currently nothing runs in parallel.
I would expect that it does not matter, if you the dependency is from something advanced to something basic. And this is where I would like to have less imports.

[mortberg]

I don't know, but currently nothing runs in parallel. I would expect that it does not matter, if you the dependency is from something advanced to something basic. And this is where I would like to have less imports.

What type of Everything/Common files would you want? I don't like for example "Algebra.Everything" because it's not very often you need all algebraic structures and it's probably good to see that the file only uses groups and rings, but "Foundations.Everything" could make sense.