*   Added a type and `Universe` for universe disjunction or summing, `:+:`,
    with appropriate `Elem` and `Auto` instances.
*   Added `Universe` instances (and appropriate `Elem` and `Auto` instances)
    for `Proxy` (the null universe) and `Identity`.
*   `Auto` instances for `IsNothing` and `IsLeft`.