*   New `:.:` for universe composition, with `Elem` and `Universe` instances,
    and associated functions for working with them alongside `Any`, `All`.
*   Many of the `Elem` instances and indices in *Data.Type.Universe* have had
    their name changed to be more consistent with their role as indices.
    `IsJust` is now `IJust`, `IsRight` is `IRight`, `Snd` is `ISnd`.
*   Convenience predicates for alternate universes, such as `IsJust`, `IsLeft`,
    `IsNothing`, etc.
*   `NotAll` quantifier added alongside `None`.
*   Many new implications added to *Data.Type.Predicate.Quantification*,
    converting not-any and all-not, etc.
*   `NotFound p` added as a convenience predicate synonym for `Not (Found p)`.
*   Some implications showing the equivalence between `Found (InP f)` and
    `NotNull f` added to *Data.Type.Predicate.Param*.
*   Many new deduction rules added to *Data.Type.Predicate.Auto*.  Please see
    module documentation for a detailed list of new rules and classes in this
    version.
*   Convenient combinators for dealing with `Refuted` and `Decision` added to
    *Data.Type.Predicate*: `elimDisproof` and `mapRefuted.