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.
Thanks, I did not know about [Proof using], there is also [Proof with].
E.g. Proof with auto allows to write [apply f...] instead of [apply f; auto.]
It is sometimes useful, although perhaps not yet in the HoTT library.