Use records, not typeclasses, for subuniverses and modalities

I have been working and thinking about these a lot and I've decided that my original idea of using typeclasses was probably not the best way: when there is more than one modality floating around then it's really better to be passing them explicitly.  This PR turns reflective subuniverses and modalities back into records.
Using something as generic as `to` for unit subuniverses makes me vaguely uneasy.  I'd be happier to have `to` be an alias (`Notation to := O_unit`) inside a `Module Import ReflectiveSubuniverseNotations` or something.  I'm open to convincing otherwise, though.