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.
I didn't really intend that either of them would be referred to explicitly under normal circumstances, so I didn't care very much what they are called.  I just shortened `msubu` because it now has to be used explicitly in the other fields, so I wanted them to be more readable.