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

The object Z represents zero.

Constructors

Instances

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

newtype S n Source

The object S n represents the successor of n.

Constructors

S
Fields unS :: n

Instances

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)

data family Omega a b :: *Source

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

data OmegaF (~>) z f Source

Constructors

Instances

class CategoryO ~> z => OmegaLimit (~>) z f whereSource

Associated Types

type OmegaL (~>) z f :: *Source

Methods

class CategoryO ~> z => OmegaColimit (~>) z f whereSource

Associated Types

type OmegaC (~>) z f :: *Source

Methods