mathlib documentation

control.uliftable

Universe lifting for type families

Some functors such as option and list are universe polymorphic. Unlike type polymorphism where option α is a function application and reasoning and generalizations that apply to functions can be used, option.{u} and option.{v} are not one function applied to two universe names but one polymorphic definition instantiated twice. This means that whatever works on option.{u} is hard to transport over to option.{v}. uliftable is an attempt at improving the situation.

uliftable option.{u} option.{v} gives us a generic and composable way to use option.{u} in a context that requires option.{v}. It is often used in tandem with ulift but the two are purposefully decoupled.

Main definitions

Tags

universe polymorphism functor

@[class]
structure uliftable  :
(Type u₀Type u₁)(Type v₀Type v₁)Type (max (u₀+1) u₁ (v₀+1) v₁)
  • congr : Π {α : Type ?} {β : Type ?}, α βf α g β

Given a universe polymorphic type family M.{u} : Type u₁ → Type u₂, this class convert between instantiations, from M.{u} : Type u₁ → Type u₂ to M.{v} : Type v₁ → Type v₂ and back

Instances
def uliftable.up {f : Type u₀Type u₁} {g : Type (max u₀ v₀)Type v₁} [uliftable f g] {α : Type u₀} :
f αg (ulift α)

The most common practical use uliftable (together with up), this function takes x : M.{u} α and lifts it to M.{max u v} (ulift.{v} α)

Equations
def uliftable.down {f : Type u₀Type u₁} {g : Type (max u₀ v₀)Type v₁} [uliftable f g] {α : Type u₀} :
g (ulift α)f α

The most common practical use of uliftable (together with up), this function takes x : M.{max u v} (ulift.{v} α) and lowers it to M.{u} α

Equations
def uliftable.adapt_up (F : Type v₀Type v₁) (G : Type (max v₀ u₀)Type u₁) [uliftable F G] [monad G] {α : Type v₀} {β : Type (max v₀ u₀)} :
F α(α → G β)G β

convenient shortcut to avoid manipulating ulift

Equations
def uliftable.adapt_down {F : Type (max u₀ v₀)Type u₁} {G : Type v₀Type v₁} [L : uliftable G F] [monad F] {α : Type (max u₀ v₀)} {β : Type v₀} :
F α(α → G β)G β

convenient shortcut to avoid manipulating ulift

Equations
def uliftable.up_map {F : Type u₀Type u₁} {G : Type (max u₀ v₀)Type v₁} [inst : uliftable F G] [functor G] {α : Type u₀} {β : Type (max u₀ v₀)} :
(α → β)F αG β

map function that moves up universes

Equations
def uliftable.down_map {F : Type (max u₀ v₀)Type u₁} {G : Type → Type v₁} [inst : uliftable G F] [functor F] {α : Type (max u₀ v₀)} {β : Type} :
(α → β)F αG β

map function that moves down universes

Equations
@[simp]
theorem uliftable.up_down {f : Type u₀Type u₁} {g : Type (max u₀ v₀)Type v₁} [uliftable f g] {α : Type u₀} (x : g (ulift α)) :

@[simp]
theorem uliftable.down_up {f : Type u₀Type u₁} {g : Type (max u₀ v₀)Type v₁} [uliftable f g] {α : Type u₀} (x : f α) :

@[instance]

Equations
def state_t.uliftable' {s : Type u₀} {s' : Type u₁} {m : Type u₀Type v₀} {m' : Type u₁Type v₁} [uliftable m m'] :
s s'uliftable (state_t s m) (state_t s' m')

for specific state types, this function helps to create a uliftable instance

Equations
@[instance]
def state_t.uliftable {s : Type u_1} {m : Type u_1Type u_2} {m' : Type (max u_1 u_3)Type u_4} [uliftable m m'] :

Equations
def reader_t.uliftable' {s : Type u_1} {s' : Type u_2} {m : Type u_1Type u_3} {m' : Type u_2Type u_4} [uliftable m m'] :
s s'uliftable (reader_t s m) (reader_t s' m')

for specific reader monads, this function helps to create a uliftable instance

Equations
@[instance]
def reader_t.uliftable {s : Type u_1} {m : Type u_1Type u_2} {m' : Type (max u_1 u_3)Type u_4} [uliftable m m'] :

Equations
def cont_t.uliftable' {r : Type u_1} {r' : Type u_2} {m : Type u_1Type u_3} {m' : Type u_2Type u_4} [uliftable m m'] :
r r'uliftable (cont_t r m) (cont_t r' m')

for specific continuation passing monads, this function helps to create a uliftable instance

Equations
@[instance]
def cont_t.uliftable {s : Type u_1} {m : Type u_1Type u_2} {m' : Type (max u_1 u_3)Type u_4} [uliftable m m'] :
uliftable (cont_t s m) (cont_t (ulift s) m')

Equations
def writer_t.uliftable' {w : Type (max u_1 u_2)} {w' : Type (max u_3 u_4)} {m : Type (max u_1 u_2)Type u_5} {m' : Type (max u_3 u_4)Type u_6} [uliftable m m'] :
w w'uliftable (writer_t w m) (writer_t w' m')

for specific writer monads, this function helps to create a uliftable instance

Equations
@[instance]
def writer_t.uliftable {s : Type (max u_1 u_2)} {m : Type (max u_1 u_2)Type u_3} {m' : Type (max (max u_1 u_2) u_4)Type u_5} [uliftable m m'] :

Equations