Portability | non-portable |
---|---|
Stability | experimental |
Maintainer | sjoerd@w3future.com |
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.
- data Z = Z
- newtype S n = S {
- unS :: n
- data family Omega a b :: *
- data OmegaF (~>) z f = OmegaF
- class CategoryO ~> z => OmegaLimit (~>) z f where
- type OmegaL (~>) z f :: *
- omegaLimit :: Limit (OmegaF ~> z f) (OmegaL ~> z f)
- class CategoryO ~> z => OmegaColimit (~>) z f where
- type OmegaC (~>) z f :: *
- omegaColimit :: Colimit (OmegaF ~> z f) (OmegaC ~> z f)
Documentation
The object Z represents zero.
Show Z | |
CategoryO Omega Z | |
Apply Omega Z Z | |
PairColimit Omega Z Z | |
PairLimit Omega Z Z | |
CategoryO Omega n => CategoryA Omega Z Z n | |
Apply Omega Z n => Apply Omega Z (S n) | |
(Coproduct Z n ~ n, PairColimit Omega Z n) => PairColimit Omega Z (S n) | |
(Product Z n ~ Z, PairLimit Omega Z n) => PairLimit Omega Z (S n) | |
CategoryA Omega Z n p => CategoryA Omega Z (S n) (S p) | |
(Coproduct n Z ~ n, PairColimit Omega n Z) => PairColimit Omega (S n) Z | |
(Product n Z ~ Z, PairLimit Omega n Z) => PairLimit Omega (S n) Z | |
CategoryO ~> z => FunctorA (OmegaF ~> z f) Z Z |
The object S n represents the successor of n.
Apply Omega Z n => Apply Omega Z (S n) | |
(Coproduct Z n ~ n, PairColimit Omega Z n) => PairColimit Omega Z (S n) | |
(Product Z n ~ Z, PairLimit Omega Z n) => PairLimit Omega Z (S n) | |
CategoryA Omega Z n p => CategoryA Omega Z (S n) (S p) | |
CategoryO Omega n => CategoryO Omega (S n) | |
(Coproduct n Z ~ n, PairColimit Omega n Z) => PairColimit Omega (S n) Z | |
(Product n Z ~ Z, PairLimit Omega n Z) => PairLimit Omega (S n) Z | |
Apply Omega a b => Apply Omega (S a) (S b) | |
PairColimit Omega a b => PairColimit Omega (S a) (S b) | |
PairLimit Omega a b => PairLimit Omega (S a) (S b) | |
CategoryA Omega n p q => CategoryA Omega (S n) (S p) (S q) | |
Show n => Show (S n) |
class CategoryO ~> z => OmegaLimit (~>) z f whereSource
omegaLimit :: Limit (OmegaF ~> z f) (OmegaL ~> z f)Source
class CategoryO ~> z => OmegaColimit (~>) z f whereSource
omegaColimit :: Colimit (OmegaF ~> z f) (OmegaC ~> z f)Source