Documentation

Mathlib.Control.ULiftable

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 #

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₁) [ULiftable f g] :

    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₁) [Functor f] [LawfulFunctor f] :
      Equations
      @[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
      Instances For
        @[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
        Instances For
          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
          Instances For
            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
            Instances For
              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
              Instances For
                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
                Instances For
                  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₀} α)) :
                  theorem ULiftable.down_up {f : Type u₀ → Type u₁} {g : Type (max u₀ v₀) → Type v₁} [ULiftable f g] {α : Type u₀} (x : f α) :
                  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'] :
                    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'] :
                    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') :
                    ULiftable (ReaderT s m) (ReaderT s' m')

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