Overhaul: weak equivalences (up to the Grad Theorem)

There is a slight problem with this pull request: changing the obvious homotopy in the type of isweqhomot to the ~ notation breaks the compilation at some commutativity type in algebra1a. This should be reviewed.

Further work will be done on the proof of pathsweq4, which I still don't completely understand.