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 was iffy about leaving in something that didn't serve any visible purpose (and might be better replaced by some more general fact), but git history has the drawback that it's not immediately visible when browsing the file, and someone later on might notice a commented-out bit and say "ah-hah, that's what I was looking for".