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.

@[implicit_reducible]

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

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

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

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

@[reducible, inline]

abbrev ULiftable.up' {f : Type u₀ → Type u₁} {g : Type v₀ → Type v₁} [ULiftable f g] : f PUnit.{u₀ + 1} → g PUnit.{v₀ + 1}

A version of up for a PUnit return type.

@[reducible, inline]

abbrev ULiftable.down' {f : Type u₀ → Type u₁} {g : Type v₀ → Type v₁} [ULiftable f g] : g PUnit.{v₀ + 1} → f PUnit.{u₀ + 1}

A version of down for a PUnit return type.

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₀} α)) : up (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 α) : down (up x) = x

@[implicit_reducible]

instance instULiftableId : ULiftable Id Id

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Option.instULiftable : ULiftable Option Option