Changing universes of types in meta-code
This file defines the meta type uchange (α : Type v) : Type u, which
permits us to change the universe of a type analogously to ulift.
However since uchange is meta, it can both lift and lower the universe.
The implementation of uchange is efficient. Both uchange.up and
uchange.down compile to no-ops.
unchecked_cast' a : β performs an unchecked cast of (a : α) to β.
Unlike unchecked_cast, it can cast across universes. The VM implementation
is guaranteed to be the identity.
@[instance]
uchange.down embeds α to uchange α.
The VM implementation is guaranteed to be the identity.
uchange.up extracts from uchange α an α.
The VM implementation is guaranteed to be the identity.