mathlib documentation

meta.uchange

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.

meta def unchecked_cast' {α : Sort u} {β : Sort v} :
α → β

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.

meta def uchange  :
Type vType 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.

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

meta def uchange.down {α : Type u_1} :
α → uchange α

uchange.down embeds α to uchange α.

The VM implementation is guaranteed to be the identity.

meta def uchange.up {α : Type u_1} :
uchange α → α

uchange.up extracts from uchange α an α.

The VM implementation is guaranteed to be the identity.