Use records, not typeclasses, for subuniverses and modalities