Data.Category.Omega

Omega, the category 0 -> 1 -> 2 -> 3 -> ... The objects are the natural numbers, and there's an arrow from a to b iff a <= b.

Documentation

data Z

data S n

data Omega where

The arrows of omega, there's an arrow from a to b iff a <= b.

Constructors

Z :: Omega Z Z

Z2S :: Omega Z n -> Omega Z (S n)

S :: Omega a b -> Omega (S a) (S b)

Instances

Category Omega

The objects of omega are the natural numbers, and there's an arrow from a to b iff a <= b.

HasInitialObject Omega

Z (zero) is the initial object of omega.

HasBinaryProducts Omega

The product in omega is the minimum.

HasBinaryCoproducts Omega

The coproduct in omega is the maximum.

zeroMonoid :: MonoidObject (CoproductFunctor Omega) Z

Zero is a monoid object wrt the maximum.

zeroComonoid :: ComonoidObject (CoproductFunctor Omega) Z

Zero is also a comonoid object wrt the maximum.