HoTT/HoTT — pull request #493 by mikeshulman (2014-09-11 23:15:24+00:00)
Title: 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.