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.