# 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 : outParam (Type u₀ → Type u₁)) (g : Type v₀ → Type v₁) :
Type (max (max (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.

f is an outParam, because g can almost always be inferred from the current monad. At any rate, the lift should be unique, as the intent is to only lift the same constants with different universe parameters.

• congr : {α : Type u₀} → {β : Type v₀} → α βf α g β
Instances
@[reducible, inline]
abbrev ULiftable.symm (f : Type u₀ → Type u₁) (g : Type v₀ → Type v₁) [] :

Not an instance as it is incompatible with outParam. In practice it seems not to be needed anyway.

Equations
Instances For
instance ULiftable.refl (f : Type u₀ → Type u₁) [] [] :
Equations
• = { congr := fun {α β : Type u₀} (e : α β) => }
@[reducible, inline]
abbrev 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), the function up.{v} takes x : M.{u} α and lifts it to M.{max u v} (ULift.{v} α)

Equations
Instances For
@[reducible, inline]
abbrev 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), the function down.{v} takes x : M.{max u v} (ULift.{v} α) and lowers it to M.{u} α

Equations
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

Equations
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

Equations
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

Equations
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

Equations
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 α) :
instance instULiftableId :
Equations
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

Equations
Instances For
instance instULiftableStateTULift {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')
Equations
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')
Equations
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

Equations
Instances For
instance instULiftableReaderTULift {s : Type u₀} {m : Type u₀ → Type u_5} {m' : Type (max u₀ u_6) → Type u_7} [ULiftable m m'] :
Equations
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'] :
Equations
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

Equations
• = { congr := fun {α : Type u_1} {β : Type u_2} => }
Instances For
instance instULiftableContTULift {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')
Equations
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')
Equations
• ContT.instULiftableULiftULift = ContT.uliftable' (Equiv.ulift.trans Equiv.ulift.symm)
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

Equations
Instances For
instance instULiftableWriterTULift {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')
Equations
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')
Equations
instance Except.instULiftable {ε : Type u₀} :
ULiftable () ()
Equations
• Except.instULiftable = { congr := fun {α : Type v₁} {β : Type v₂} (e : α β) => { toFun := , invFun := Except.map e.symm, left_inv := , right_inv := } }
Equations