Clean up library

[thomas-lamiaux]

This pull request is a one week effort to clean the library

It will focus on :

• Enforcing some of the naming convention (global and algebra) decided last week in past files.
  In particular the ones about import.
• Renaming some object ill named.
• Split of merge some files to enhanced clarity.

However, the goal is not to add any content to the library.
Don't hesitate to comment for instance to tell me to look at something

Description of the pull request :

• Cleaning Polynomials
• Renaming the PropositionalTruncation (description below)
• Cleaning ZCohomology import, and some other files
• Enforcing naming convention for Group and CommRing
• Getting rid of open import Cubical.Foundations.Everything except in one paper in which the import are so messy that I preferred not to touch it. resolve Files should not import Everything files unless necessary #570
• Rename Direct-Sum to DirectSum

[thomas-lamiaux]

The proposition truncation was named ||||, ||, squash. It was done according to the HoTT Book.
However, for set and more it is indexed by the number for instance for set it is ||_||_2

The issue is that a numerous (like at least 50 and many complicated ones) are mixing more than one level of set truncation.
In which case, it is really better and clearer to always index them.
This actually what is already done in a bunch of files though with different notation.

Plus the notation for general truncation and proposition truncation is the same !
Some files are mixing the two. Sometimes even without renaming the prop one.
This makes files harder to read and even sometimes unreadable.

To solve this issue, I have rewritten textually (ie not with "renaming (X to Y)) the library with the convention where it is indexed in specific case so ||_||_1 etc...
The modification are without a doubt uninteresting.

[mortberg]

Great! I think we should merge now, or is there some PR that should be merged first? @ecavallo @felixwellen

[mortberg]

Merging!