Data.Category.Peano

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

Documentation

data Peano where

Constructors

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

Instances

Category ~> => Category (Peano ~>)

HasInitialObject (Peano (->))

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.