Data.Category.NNO

Documentation

class HasTerminalObject k => HasNaturalNumberObject k where

Minimal complete definition

zero, succ, primRec

Associated Types

type NaturalNumberObject k :: *

Methods

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

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

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

Instances

HasNaturalNumberObject (->)

Associated Types

type NaturalNumberObject ((->) :: * -> * -> *) :: *

Methods

zero :: TerminalObject (->) -> NaturalNumberObject (->)

succ :: NaturalNumberObject (->) -> NaturalNumberObject (->)

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

HasNaturalNumberObject Cat

Associated Types

type NaturalNumberObject (Cat :: * -> * -> *) :: *

Methods

zero :: Cat (TerminalObject Cat) (NaturalNumberObject Cat)

succ :: Cat (NaturalNumberObject Cat) (NaturalNumberObject Cat)

primRec :: Cat (TerminalObject Cat) a -> Cat a a -> Cat (NaturalNumberObject Cat) a

data NatNum

Constructors

Z

S NatNum

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

data PrimRec z s

Constructors

PrimRec z s

Instances

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

Associated Types

type Dom (PrimRec z s) :: * -> * -> *

type Cod (PrimRec z s) :: * -> * -> *

type (PrimRec z s) :% a :: *

Methods

(%) :: PrimRec z s -> Dom (PrimRec z s) a b -> Cod (PrimRec z s) (PrimRec z s :% a) (PrimRec z s :% b)

type Dom (PrimRec z s)

type Dom (PrimRec z s) = Nat

type Cod (PrimRec z s)

type Cod (PrimRec z s) = Cod z

type (PrimRec z s) :% (I1 ())

type (PrimRec z s) :% (I1 ()) = (:%) z ()

type (PrimRec z s) :% (I2 n)

type (PrimRec z s) :% (I2 n) = (:%) s ((:%) (PrimRec z s) n)