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.
You should probably rename anything that involves the old `SubuniverseStruct` name.