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

Equations

• ULiftable.symm f g = { congr := fun {α} {β} e => (ULiftable.congr e.symm).symm }

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

Equations

• ULiftable.up = (ULiftable.congr Equiv.ulift.symm).toFun

@[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} α

Equations

• ULiftable.down = (ULiftable.congr Equiv.ulift.symm).invFun

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

Equations

• ULiftable.adaptUp F G x f = ULiftable.up x >>= f ∘ ULift.down

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

Equations

• ULiftable.adaptDown x f = ULiftable.down (x >>= ULiftable.up ∘ f)

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

Equations

• ULiftable.upMap f x = (f ∘ ULift.down) <$> ULiftable.up x

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

Equations

• ULiftable.downMap f x = ULiftable.down ((ULift.up ∘ f) <$> x)

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

Equations

• instULiftableId = { congr := fun {α} {β} F => 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

Equations

• StateT.uliftable' F = { congr := fun {α} {β} G => StateT.equiv (Equiv.piCongr F fun x => ULiftable.congr (Equiv.prodCongr G F)) }

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')

Equations

• instULiftableStateTStateTULift = StateT.uliftable' Equiv.ulift.symm

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')

Equations

• StateT.instULiftableULiftULift = StateT.uliftable' (Equiv.ulift.trans Equiv.ulift.symm)

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

Equations

• ReaderT.uliftable' F = { congr := fun {α} {β} G => ReaderT.equiv (Equiv.piCongr F fun x => ULiftable.congr G) }

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')

Equations

• instULiftableReaderTReaderTULift = ReaderT.uliftable' Equiv.ulift.symm

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')

Equations

• ReaderT.instULiftableULiftULift = ReaderT.uliftable' (Equiv.ulift.trans Equiv.ulift.symm)

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

• ContT.uliftable' F = { congr := fun {α} {β} => ContT.equiv (ULiftable.congr F) }

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')

Equations

• instULiftableContTContTULift = ContT.uliftable' Equiv.ulift.symm

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')

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

• WriterT.uliftable' F = { congr := fun {α} {β} G => WriterT.equiv (ULiftable.congr (Equiv.prodCongr G F)) }

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')

Equations

• instULiftableWriterTWriterTULift = WriterT.uliftable' Equiv.ulift.symm

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')

Equations

• WriterT.instULiftableULiftULift = WriterT.uliftable' (Equiv.ulift.trans Equiv.ulift.symm)

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

Equations

• One or more equations did not get rendered due to their size.

instance Option.instULiftable : ULiftable Option Option

Equations

• One or more equations did not get rendered due to their size.