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.
Minor: Is there a reason to name these?  For consistency with the rest of the library, if you do name them, they should probably be named `ua` and `fs`, but this isn't that important, and shouldn't block merging this.