Renamed some files. Moved some stuff around. Began writing something
on erasure.
Tried to proof proof irrelevance to be equivalent to hprop.
Wrote a bit more stuff on erasure.