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
uchange is meta, it can both lift and lower the universe.
uchange (α : Sort v) : Sort u is an equivalent type in a different universe.
In the VM, both
uchange α have the same representation.
This definition is
meta because it collapses the universe hierarchy; if pure code could do
this then one could derive Girard's paradox.