# Documentation

Mathlib.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 #

• ULiftable class

## Tags #

universe polymorphism functor

class ULiftable (f : Type u₀ → Type u₁) (g : Type v₀ → Type v₁) :
Type (max (max (max (u₀ + 1) u₁) (v₀ + 1)) v₁)
• congr : {α : Type u₀} → {β : Type v₀} → α β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
instance ULiftable.symm (f : Type u₀ → Type u₁) (g : Type v₀ → Type v₁) [] :
@[reducible]
def ULiftable.up {f : Type u₀ → Type u₁} {g : Type (max u₀ v₀) → Type v₁} [] {α : Type u₀} :
f αg ()

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

Instances For
@[reducible]
def ULiftable.down {f : Type u₀ → Type u₁} {g : Type (max u₀ v₀) → Type v₁} [] {α : Type u₀} :
g ()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} α

Instances For
def ULiftable.adaptUp (F : Type v₀ → Type v₁) (G : Type (max v₀ u₀) → Type u₁) [] [] {α : Type v₀} {β : Type (max v₀ u₀)} (x : F α) (f : αG β) :
G β

convenient shortcut to avoid manipulating ULift

Instances For
def ULiftable.adaptDown {F : Type (max u₀ v₀) → Type u₁} {G : Type v₀ → Type v₁} [L : ] [] {α : Type (max u₀ v₀)} {β : Type v₀} (x : F α) (f : αG β) :
G β

convenient shortcut to avoid manipulating ULift

Instances For
def ULiftable.upMap {F : Type u₀ → Type u₁} {G : Type (max u₀ v₀) → Type v₁} [] [] {α : Type u₀} {β : Type (max u₀ v₀)} (f : αβ) (x : F α) :
G β

map function that moves up universes

Instances For
def ULiftable.downMap {F : Type (max u₀ v₀) → Type u₁} {G : Type u₀ → Type v₁} [] [] {α : Type (max u₀ v₀)} {β : Type u₀} (f : αβ) (x : F α) :
G β

map function that moves down universes

Instances For
theorem ULiftable.up_down {f : Type u₀ → Type u₁} {g : Type (max u₀ v₀) → Type v₁} [] {α : Type u₀} (x : g ()) :
theorem ULiftable.down_up {f : Type u₀ → Type u₁} {g : Type (max u₀ v₀) → Type v₁} [] {α : Type u₀} (x : f α) :
def StateT.uliftable' {s : Type u₀} {s' : Type u₁} {m : Type u₀ → Type v₀} {m' : Type u₁ → Type v₁} [ULiftable m m'] (F : s s') :
ULiftable (StateT s m) (StateT s' m')

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

Instances For
instance instULiftableStateTStateTULift {s : Type u₀} {m : Type u₀ → Type u_5} {m' : Type (max u₀ u_6) → Type u_7} [ULiftable m m'] :
ULiftable (StateT s m) (StateT () m')
instance StateT.instULiftableULiftULift {s : Type u₀} {m : Type (max u₀ v₀) → Type u_5} {m' : Type (max u₀ v₁) → Type u_6} [ULiftable m m'] :
ULiftable (StateT () m) (StateT () m')
def ReaderT.uliftable' {s : Type u₀} {s' : Type u₁} {m : Type u₀ → Type u_5} {m' : Type u₁ → Type u_6} [ULiftable m m'] (F : s s') :

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

Instances For
instance instULiftableReaderTReaderTULift {s : Type u₀} {m : Type u₀ → Type u_5} {m' : Type (max u₀ u_6) → Type u_7} [ULiftable m m'] :
instance ReaderT.instULiftableULiftULift {s : Type u₀} {m : Type (max u₀ v₀) → Type u_5} {m' : Type (max u₀ v₁) → Type u_6} [ULiftable m m'] :
def ContT.uliftable' {r : Type u_1} {r' : Type u_2} {m : Type u_1 → Type u_5} {m' : Type u_2 → Type u_6} [ULiftable m m'] (F : r r') :
ULiftable (ContT r m) (ContT r' m')

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

Instances For
instance instULiftableContTContTULift {s : Type u_5} {m : Type u_5 → Type u_6} {m' : Type (max u_5 u_7) → Type u_8} [ULiftable m m'] :
ULiftable (ContT s m) (ContT () m')
instance ContT.instULiftableULiftULift {s : Type u₀} {m : Type (max u₀ v₀) → Type u_5} {m' : Type (max u₀ v₁) → Type u_6} [ULiftable m m'] :
ULiftable (ContT () m) (ContT () m')
def WriterT.uliftable' {w : Type u_3} {w' : Type u_4} {m : Type u_3 → Type u_5} {m' : Type u_4 → Type u_6} [ULiftable m m'] (F : w w') :
ULiftable (WriterT w m) (WriterT w' m')

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

Instances For
instance instULiftableWriterTWriterTULift {s : Type u₀} {m : Type u₀ → Type u_5} {m' : Type (max u₀ u_6) → Type u_7} [ULiftable m m'] :
ULiftable (WriterT s m) (WriterT () m')
instance WriterT.instULiftableULiftULift {s : Type u₀} {m : Type (max u₀ v₀) → Type u_5} {m' : Type (max u₀ v₁) → Type u_6} [ULiftable m m'] :
ULiftable (WriterT () m) (WriterT () m')
instance Except.instULiftable {ε : Type u₀} :
ULiftable () ()