Data.Category.Peano

A Peano category as in When is one thing equal to some other thing? Barry Mazur, 2007

Documentation

data PeanoO (~>) a where

Constructors

PeanoO :: (TerminalObject ~> ~> x) -> (x ~> x) -> PeanoO ~> x

data Peano where

Constructors

PeanoA :: PeanoO ~> a -> PeanoO ~> b -> (a ~> b) -> Peano ~> a b

Instances

HasTerminalObject ~> => Category (Peano ~>)

HasInitialObject (Peano (->))

peanoId :: Category ~> => PeanoO ~> a -> Obj (Peano ~>) a

peanoO :: Category ~> => Obj (Peano ~>) a -> PeanoO ~> a

data NatNum

The natural numbers are the initial object for the Peano category.

Constructors

Z ()

S NatNum

primRec :: (() -> t) -> (t -> t) -> NatNum -> t

Primitive recursion is the factorizer from the natural numbers.