module Data.Category.Omega where
import Prelude hiding ((.), id, Functor, product)
import Data.Category
import Data.Category.Limit
data Z
data S n
data Omega :: * -> * -> * where
IdZ :: Omega Z Z
GTZ :: Omega Z n -> Omega Z (S n)
StS :: Omega a b -> Omega (S a) (S b)
instance Category Omega where
data Obj Omega a where
OZ :: Obj Omega Z
OS :: Obj Omega n -> Obj Omega (S n)
src IdZ = OZ
src (GTZ _) = OZ
src (StS a) = OS (src a)
tgt IdZ = OZ
tgt (GTZ a) = OS (tgt a)
tgt (StS a) = OS (tgt a)
id OZ = IdZ
id (OS n) = StS (id n)
a . IdZ = a
(StS a) . (GTZ n) = GTZ (a . n)
(StS a) . (StS b) = StS (a . b)
_ . _ = error "Other combinations should not type check"
instance HasInitialObject Omega where
type InitialObject Omega = Z
initialObject = OZ
initialize OZ = IdZ
initialize (OS n) = GTZ $ initialize n
type instance BinaryProduct Omega Z n = Z
type instance BinaryProduct Omega n Z = Z
type instance BinaryProduct Omega (S a) (S b) = S (BinaryProduct Omega a b)
instance HasBinaryProducts Omega where
product OZ _ = OZ
product _ OZ = OZ
product (OS a) (OS b) = OS (product a b)
proj OZ OZ = (IdZ, IdZ)
proj OZ (OS n) = (IdZ, GTZ . snd $ proj OZ n)
proj (OS n) OZ = (GTZ . fst $ proj n OZ, IdZ)
proj (OS a) (OS b) = (StS proj1, StS proj2) where (proj1, proj2) = proj a b
IdZ &&& _ = IdZ
_ &&& IdZ = IdZ
GTZ a &&& GTZ b = GTZ (a &&& b)
StS a &&& StS b = StS (a &&& b)
_ &&& _ = error "Other combinations should not type check"
type instance BinaryCoproduct Omega Z n = n
type instance BinaryCoproduct Omega n Z = n
type instance BinaryCoproduct Omega (S a) (S b) = S (BinaryCoproduct Omega a b)
instance HasBinaryCoproducts Omega where
coproduct OZ n = n
coproduct n OZ = n
coproduct (OS a) (OS b) = OS (coproduct a b)
inj OZ OZ = (IdZ, IdZ)
inj OZ (OS n) = (GTZ inj1, StS inj2) where (inj1, inj2) = inj OZ n
inj (OS n) OZ = (StS inj1, GTZ inj2) where (inj1, inj2) = inj n OZ
inj (OS a) (OS b) = (StS inj1, StS inj2) where (inj1, inj2) = inj a b
IdZ ||| IdZ = IdZ
GTZ _ ||| a = a
a ||| GTZ _ = a
StS a ||| StS b = StS (a ||| b)
_ ||| _ = error "Other combinations should not type check"
instance Show (Obj Omega a) where
show OZ = "OZ"
show (OS n) = "OS " ++ show n