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

instance ULiftable.symm (f : Type u₀ → Type u₁) (g : Type v₀ → Type v₁) [ULiftable f g] : ULiftable g f

@[reducible]

def ULiftable.up {f : Type u₀ → Type u₁} {g : Type (max u₀ v₀) → Type v₁} [ULiftable f g] {α : Type u₀} : f α → g (ULift.{v₀, u₀} α)

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} α)

@[reducible]

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

def ULiftable.adaptUp (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

def ULiftable.adaptDown {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

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

map function that moves up universes

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

map function that moves down universes

theorem ULiftable.up_down {f : Type u₀ → Type u₁} {g : Type (max u₀ v₀) → Type v₁} [ULiftable f g] {α : Type u₀} (x : g (ULift.{v₀, u₀} α)) : ULiftable.up (ULiftable.down x) = x

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

instance instULiftableId : ULiftable Id Id

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

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 (ULift.{u_6, u₀} s) 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 (ULift.{max v₀ u₀, u₀} s) m) (StateT (ULift.{max v₁ u₀, u₀} s) 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') : ULiftable (ReaderT s m) (ReaderT s' m')

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

instance instULiftableReaderTReaderTULift {s : Type u₀} {m : Type u₀ → Type u_5} {m' : Type (max u₀ u_6) → Type u_7} [ULiftable m m'] : ULiftable (ReaderT s m) (ReaderT (ULift.{u_6, u₀} s) 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'] : ULiftable (ReaderT (ULift.{max v₀ u₀, u₀} s) m) (ReaderT (ULift.{max v₁ u₀, u₀} s) 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

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 (ULift.{u_7, u_5} s) 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 (ULift.{max v₀ u₀, u₀} s) m) (ContT (ULift.{max v₁ u₀, u₀} s) 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

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 (ULift.{u_6, u₀} s) 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 (ULift.{max v₀ u₀, u₀} s) m) (WriterT (ULift.{max v₁ u₀, u₀} s) m')

instance Except.instULiftable {ε : Type u₀} : ULiftable (Except ε) (Except ε)

instance Option.instULiftable : ULiftable Option Option