Type.Data.Num.Unary
data Unary
data Un x
data Zero
data Succ x
zero
succ
data Singleton n
singleton
singletonFromProxy
integerFromSingleton
integralFromSingleton
class Natural n
class Positive n
type family x :+: y
type family x :*: y