module Data.Category.Peano where
import Prelude(($))
import Data.Category
import Data.Category.Limit
data Peano :: (* -> * -> *) -> * -> * -> * where
PeanoA :: Obj (Peano (~>)) a -> Obj (Peano (~>)) b -> (a ~> b) -> Peano (~>) a b
instance Category (~>) => Category (Peano (~>)) where
data Obj (Peano (~>)) a where
PeanoO :: Obj (~>) x -> x -> (x ~> x) -> Obj (Peano (~>)) x
src (PeanoA s _ _) = s
tgt (PeanoA _ t _) = t
id p@(PeanoO x _ _) = PeanoA p p $ id x
(PeanoA _ t f) . (PeanoA s _ g) = PeanoA s t $ f . g
data NatNum = Z | S NatNum
primRec :: t -> (t -> t) -> NatNum -> t
primRec z _ Z = z
primRec z s (S n) = s (primRec z s n)
instance HasInitialObject (Peano (->)) where
type InitialObject (Peano (->)) = NatNum
initialObject = PeanoO HaskO Z S
initialize o@(PeanoO HaskO z s) = PeanoA initialObject o $ primRec z s