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 β

@[reducible, inline]

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

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

Equations

• ULiftable.symm f g = { congr := fun {α : Type v₀} {β : Type u₀} (e : α ≃ β) => (ULiftable.congr e.symm).symm }

instance ULiftable.refl (f : Type u₀ → Type u₁) [Functor f] [LawfulFunctor f] : ULiftable f f

Equations

• ULiftable.refl f = { congr := fun {α β : Type u₀} (e : α ≃ β) => Functor.mapEquiv f e }

@[reducible, inline]

abbrev 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), the function up.{v} takes x : M.{u} α and lifts it to M.{max u v} (ULift.{v} α)

Equations

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

@[reducible, inline]

abbrev 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), the function down.{v} 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 {α : Type u_5} {β : Type u_6} (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 {α : Type u₀} {β : Type u₁} (G : α ≃ β) => StateT.equiv (F.piCongr fun (x : s) => ULiftable.congr (G.prodCongr F)) }

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

Equations

• instULiftableStateTULift = 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 {α : Type u₀} {β : Type u₁} (G : α ≃ β) => ReaderT.equiv (F.piCongr fun (x : s) => ULiftable.congr G) }

instance instULiftableReaderTULift {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

• instULiftableReaderTULift = 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 {α : Type u_1} {β : Type u_2} => ContT.equiv (ULiftable.congr F) }

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 (ULift.{u_7, u_5} s) m')

Equations

• instULiftableContTULift = 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 {α : Type u_3} {β : Type u_4} (G : α ≃ β) => WriterT.equiv (ULiftable.congr (G.prodCongr F)) }

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

Equations

• instULiftableWriterTULift = 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

• Except.instULiftable = { congr := fun {α : Type v₁} {β : Type v₂} (e : α ≃ β) => { toFun := Except.map ⇑e, invFun := Except.map ⇑e.symm, left_inv := ⋯, right_inv := ⋯ } }

instance Option.instULiftable : ULiftable Option Option

Equations

• Option.instULiftable = { congr := fun {α : Type u₀} {β : Type u₁} (e : α ≃ β) => { toFun := Option.map ⇑e, invFun := Option.map ⇑e.symm, left_inv := ⋯, right_inv := ⋯ } }