Include useful redundant data in modalities

This adds to a `ReflectiveSubuniverse` the data of a predicate to be in the subuniverse, and to `Modality` the data of a general induction principle into modal types.  These can be defined, up to equivalence, from the data that used to be there, but in some examples (like `Truncation`) one or both of these data occur naturally in a way that is judgmentally different from (and better than) the one that can be constructed from the other data.  So I think it's better to include them as extra redundant data, with "easy" constructors that fill them in automatically if desired.  In particular, this fixes the problem Jason noticed in Freudenthal.  I think this is analogous to our choice to define `IsEquiv` using half-adjoint equivalences rather than, say, contractible fibers, so that the inverse function would be remembered as explicit data.
The other stuff was "let me see how far I can get before giving up".  And then I saw `Truncation` and `Modality` stuff, and figured that I could point to that, and should stop trying to prove it manually.