data Singleton : a -> Type
The type containing only a particular value.
This is useful for calculating type-level information at runtime.
unVal : Singleton x -> a
.unVal : Singleton x -> a
pure : (x : a) -> Singleton x
(<*>) : Singleton f -> Singleton x -> Singleton (f x)