mathlib3 documentation

control.uliftable

Universe lifting for type families #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
@[class]
structure uliftable (f : Type u₀ → Type u₁) (g : Type v₀ → Type v₁) :
Type (max (u₀+1) u₁ (v₀+1) v₁)

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 of this typeclass
Instances of other typeclasses for uliftable
  • uliftable.has_sizeof_inst
source
@[reducible]
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
source
@[reducible]
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
source
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₀)} (x : F α) (f : α → G β) :
G β

convenient shortcut to avoid manipulating ulift

Equations
source
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₀} (x : F α) (f : α → G β) :
G β

convenient shortcut to avoid manipulating ulift

Equations
source
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 : α → β) (x : F α) :
G β

map function that moves up universes

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

map function that moves down universes

Equations
source
@[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 α)) :
uliftable.up (uliftable.down x) = x
source
@[simp]
theorem uliftable.down_up {f : Type u₀ → Type u₁} {g : Type (max u₀ v₀) → Type v₁} [uliftable f g] {α : Type u₀} (x : f α) :
uliftable.down (uliftable.up x) = x
source
@[protected, instance]
def id.uliftable  :
uliftable id id
Equations
source
def state_t.uliftable' {s : Type u₀} {s' : Type u₁} {m : Type u₀ → Type v₀} {m' : Type u₁ → Type v₁} [uliftable m m'] (F : s ≃ s') :
uliftable (state_t s m) (state_t s' m')

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

Equations
source
@[protected, instance]
def state_t.uliftable {s : Type u₀} {m : Type u₀ → Type u_1} {m' : Type (max u₀ u_2) → Type u_3} [uliftable m m'] :
uliftable (state_t s m) (state_t (ulift s) m')
Equations
source
def reader_t.uliftable' {s : Type u₀} {s' : Type u₁} {m : Type u₀ → Type u_1} {m' : Type u₁ → Type u_2} [uliftable m m'] (F : s ≃ s') :
uliftable (reader_t s m) (reader_t s' m')

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

Equations
source
@[protected, instance]
def reader_t.uliftable {s : Type u₀} {m : Type u₀ → Type u_1} {m' : Type (max u₀ u_2) → Type u_3} [uliftable m m'] :
uliftable (reader_t s m) (reader_t (ulift s) m')
Equations
source
def cont_t.uliftable' {r : Type u_1} {r' : Type u_2} {m : Type u_1 → Type u_3} {m' : Type u_2 → Type u_4} [uliftable m m'] (F : 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
source
@[protected, instance]
def cont_t.uliftable {s : Type u_1} {m : Type u_1 → Type 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
source
def writer_t.uliftable' {w : Type u_3} {w' : Type u_4} {m : Type u_3 → Type u_1} {m' : Type u_4 → Type u_2} [uliftable m m'] (F : w ≃ w') :
uliftable (writer_t w m) (writer_t w' m')

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

Equations
source
@[protected, instance]
def writer_t.uliftable {s : Type u₀} {m : Type u₀ → Type u_1} {m' : Type (max u₀ u_2) → Type u_3} [uliftable m m'] :
uliftable (writer_t s m) (writer_t (ulift s) m')
Equations