HoTT/HoTT — pull request #393 by KevinQuirin (2014-05-15 14:58:09+00:00)
Title: Reflexive subuniverses

I formalized the definition and some theorems about reflexive subuniverses (Chapter 7.7). I tried to follow proofs from the book as much as possible, so some coq proof aren't very elegant.

I had to add a lemma to Equivalences.v, and a lemma to PathGroupoids.v.