Data.Category.NNO

Documentation

class HasTerminalObject k => HasNaturalNumberObject k where

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 ((->) :: Type -> Type -> Type)

Defined in Data.Category.NNO

Associated Types

type NaturalNumberObject (->) :: Type

Methods

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

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

primRec :: (TerminalObject (->) -> a) -> (a -> a) -> NaturalNumberObject (->) -> 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)

Defined in Data.Category.NNO

Associated Types

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

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

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

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)

Defined in Data.Category.NNO

type Dom (PrimRec z s) = Nat

type Cod (PrimRec z s)

Defined in Data.Category.NNO

type Cod (PrimRec z s) = Cod z

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

Defined in Data.Category.NNO

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

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

Defined in Data.Category.NNO

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