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.

source

@[irreducible]

meta def unchecked_cast' {α : Sort u} {β : Sort v} (a : α) :

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.

source

meta def uchange (α : Type v) :

Type u

uchange (α : Sort v) : Sort u is an equivalent type in a different universe.

In the VM, both α and 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.

source

@[protected, instance]

meta def uchange.decidable_eq {α : Type v} [decidable_eq α] :

decidable_eq (uchange α)

source

meta def uchange.down {α : Type u_1} (a : α) :

uchange α

uchange.down embeds α to uchange α.

The VM implementation is guaranteed to be the identity.

source

meta def uchange.up {α : Type u_1} (a : uchange α) :

uchange.up extracts from uchange α an α.

The VM implementation is guaranteed to be the identity.