Reflective subuniverses

I formalized the definition and some theorems about reflective subuniverses (Chapter 7.7). I tried to follow proofs from the book as much as possible, so some coq proof aren't very elegant.

> Bas, I hope this is the correct way to comment on a comment:
> It is OK to improve on the proofs from the book.

I had to add a lemma to Equivalences.v, and a lemma to PathGroupoids.v.
I didn't used implicit arguments for the reflective subuniverse part, so "Set Implicit Argument" is into the section Modalities, line 14.