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.
What's the point of making such a promise?  Yes, evidently univalence is now getting used somewhere, which is a little surprising; I haven't taken the time to figure out where or why.