{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
module CCC where

data Cat k a b where
  ID :: Cat k a a
  Comp :: k b c -> k a b -> Cat k a c

data Cartesian k a b where
  Prod :: k a c -> k a d -> Cartesian k a (c, d)
  ExL :: Cartesian k (a, b) a
  ExR :: Cartesian k (a, b) b

data Terminal k a b where
  Terminal :: Terminal k a ()

data Boolean k a b where
  BTrue :: Boolean k () Bool
  BFalse :: Boolean k () Bool
  BNot :: Boolean k Bool Bool
  BImp :: Boolean k (Bool, Bool) Bool

data OneOf' xs k a b where
  OneZ :: f k a b -> OneOf' (f ': xs) k a b
  OneS :: OneOf' xs k a b -> OneOf' (x ': xs) k a b

newtype Fix2 f a b = Fix2 { unFix2 :: f (Fix2 f) a b }

type OneOf xs = Fix2 (OneOf' xs)

type CCCBool = OneOf '[Cat, Cartesian, Terminal, Boolean]