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.
Do we want to add `Notation "T ∈ O" := (In O T)` to Utf8?  And do we want to add `Notation "T \in O"` to this file?