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.
It might be slightly nicer to have
```coq
symmetry.
exact (ap10 (wedge_incl_comp1 x0 x0 _ _ _ _ x) r).
```
rather than
```coq
    unfold wedge_incl_elim_uncurried.
    simpl.
    apply symmetry.
    etransitivity.
    refine (ap10 (wedge_incl_comp1 x0 x0 _ _ _ _ x) r).
    unfold FST_Codes_cross_x0.
    reflexivity.
```