replaced hProp by UU
removed transportf_idpath
removed isofhlevelonestep
changed name of a lemma
changed proof of two lemmas to instances of some of Vladis lemmas