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.
This is true.  But it is easier to read things if you don't need to look up what everything means.  Do you think the brevity of `to` helps readability by being short more than it hinders it by being non-obvious/non-descriptive?