Uniformize reflective subuniverses and modalities

And also add a few more examples.  This closes #457.  The use of typeclasses is a bit hackish (see comments in `ReflectiveSubuniverse.v`), but it's the best way I've been able to think of to avoid having to pass the modality as an argument to everything all the time when there is only one modality hanging around.
I intentionally decided not to use `:>` for typeclasses because it is confusing (I'm planning to put this in the style guide as well).  For records, `:>` means a coercion, but for typeclasses, it means an instance; so I spent a while being confused about why the `:>` in my typeclasses wasn't creating a coercion.  Declaring both the existing instance and the coercion explicitly is clearer.