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