module Data.Category.Fix where
import Data.Category
import Data.Category.Functor
import Data.Category.Limit
import Data.Category.CartesianClosed
import Data.Category.Unit
import Data.Category.Coproduct
newtype Fix f a b = Fix (f (Fix f) a b)
instance Category (f (Fix f)) => Category (Fix f) where
src (Fix a) = Fix (src a)
tgt (Fix a) = Fix (tgt a)
Fix a . Fix b = Fix (a . b)
instance HasInitialObject (f (Fix f)) => HasInitialObject (Fix f) where
type InitialObject (Fix f) = InitialObject (f (Fix f))
initialObject = Fix initialObject
initialize (Fix o) = Fix (initialize o)
instance HasTerminalObject (f (Fix f)) => HasTerminalObject (Fix f) where
type TerminalObject (Fix f) = TerminalObject (f (Fix f))
terminalObject = Fix terminalObject
terminate (Fix o) = Fix (terminate o)
instance HasBinaryProducts (f (Fix f)) => HasBinaryProducts (Fix f) where
type BinaryProduct (Fix f) a b = BinaryProduct (f (Fix f)) a b
proj1 (Fix a) (Fix b) = Fix (proj1 a b)
proj2 (Fix a) (Fix b) = Fix (proj2 a b)
Fix a &&& Fix b = Fix (a &&& b)
instance HasBinaryCoproducts (f (Fix f)) => HasBinaryCoproducts (Fix f) where
type BinaryCoproduct (Fix f) a b = BinaryCoproduct (f (Fix f)) a b
inj1 (Fix a) (Fix b) = Fix (inj1 a b)
inj2 (Fix a) (Fix b) = Fix (inj2 a b)
Fix a ||| Fix b = Fix (a ||| b)
instance CartesianClosed (f (Fix f)) => CartesianClosed (Fix f) where
type Exponential (Fix f) a b = Exponential (f (Fix f)) a b
apply (Fix a) (Fix b) = Fix (apply a b)
tuple (Fix a) (Fix b) = Fix (tuple a b)
Fix a ^^^ Fix b = Fix (a ^^^ b)
data Wrap (f :: (* -> * -> *) -> * -> * -> *) = Wrap
instance Category (f (Fix f)) => Functor (Wrap f) where
type Dom (Wrap f) = f (Fix f)
type Cod (Wrap f) = Fix f
type Wrap f :% a = a
Wrap % f = Fix f
type Omega = Fix ((:>>:) Unit)