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.
Why `msubu` but `mod_replete`?  (Is it just that `msubu` is used more often?  An is there any reason to use `mod_replete` rather than `modality_replete`?