HoTT/HoTT-Agda — pull request #13 by mikeshulman (2014-06-07 04:41:40+00:00)
Title: Add some lemmas

I'm new at contributing to this repository, so please let me know if I violated any conventions. One thing I wasn't sure about was that in promoting the 'aux' lemmas from Univalence into public named ones, I thought they would go better in PathOver, but putting them there required reordering the imports.