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