data-category-0.5.0: Category theory

Portabilitynon-portable
Stabilityexperimental
Maintainersjoerd@w3future.com
Safe HaskellSafe-Inferred

Data.Category.NNO

Description

 

Documentation

class HasTerminalObject k => HasNaturalNumberObject k whereSource

Associated Types

type NaturalNumberObject k :: *Source

Methods

zero :: k (TerminalObject k) (NaturalNumberObject k)Source

succ :: k (NaturalNumberObject k) (NaturalNumberObject k)Source

primRec :: k (TerminalObject k) a -> k a a -> k (NaturalNumberObject k) aSource

Instances

data NatNum Source

Constructors

Z 
S NatNum 

type Nat = Fix (:++: Unit)Source

data PrimRec z s Source

Constructors

PrimRec z s 

Instances

(Category (Dom (PrimRec z s)), Category (Cod (PrimRec z s)), Functor z, Functor s, ~ (* -> * -> *) (Dom z) Unit, ~ (* -> * -> *) (Cod z) (Dom s), ~ (* -> * -> *) (Dom s) (Cod s)) => Functor (PrimRec z s)