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.
We have here a typical dychotomy between how mathematicians use symbols and how computer scientits do it. In software development it is almost always better to err on the side of descriptive names, while mathematicians like to name everything with a single letter, even at the expense of using multiple alphabets, fonts, decorations, etc.