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