data-category-0.2.0: Restricted categories

Portabilitynon-portable
Stabilityexperimental
Maintainersjoerd@w3future.com

Data.Category.Omega

Description

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.

Synopsis

Documentation

data Z Source

data S n Source

data Omega whereSource

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

Constructors

IdZ :: Omega Z Z 
GTZ :: Omega Z n -> Omega Z (S n) 
StS :: Omega a b -> Omega (S a) (S b)