module Data.Category.Peano where
import Prelude(($))
import Data.Category
import Data.Category.Limit
data PeanoO (~>) a where
PeanoO :: (TerminalObject (~>) ~> x) -> (x ~> x) -> PeanoO (~>) x
data Peano :: (* -> * -> *) -> * -> * -> * where
PeanoA :: PeanoO (~>) a -> PeanoO (~>) b -> (a ~> b) -> Peano (~>) a b
peanoId :: Category (~>) => PeanoO (~>) a -> Obj (Peano (~>)) a
peanoId o@(PeanoO z _) = PeanoA o o $ tgt z
peanoO :: Category (~>) => Obj (Peano (~>)) a -> PeanoO (~>) a
peanoO (PeanoA o _ _) = o
instance HasTerminalObject (~>) => Category (Peano (~>)) where
src (PeanoA s _ _) = peanoId s
tgt (PeanoA _ t _) = peanoId t
(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 = peanoId $ PeanoO Z S
initialize (peanoO -> o@(PeanoO z s)) = PeanoA (peanoO initialObject) o $ primRec z s