UniMath/UniMath — pull request #66 by lambdabetaheta (2014-12-18 23:49:08+00:00)
Title: 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.