module Data.Category.Void where
import Prelude hiding ((.), id, Functor)
import Data.Category
import Data.Category.Functor
import Data.Category.NaturalTransformation
data Void a b
magicVoid :: Void a b -> x
magicVoid x = x `seq` error "we never get this far"
magicVoidO :: Obj Void a -> x
magicVoidO x = x `seq` error "we never get this far"
instance Category Void where
data Obj Void a
src = magicVoid
tgt = magicVoid
id = magicVoidO
a . b = magicVoid (a `seq` b)
data VoidDiagram ((~>) :: * -> * -> *) = VoidDiagram
type instance Dom (VoidDiagram (~>)) = Void
type instance Cod (VoidDiagram (~>)) = (~>)
instance Functor (VoidDiagram (~>)) where
VoidDiagram %% x = magicVoidO x
VoidDiagram % f = magicVoid f
voidNat :: (Functor f, Functor g, Dom f ~ Void, Dom g ~ Void, Cod f ~ d, Cod g ~ d)
=> f -> g -> Nat Void d f g
voidNat f g = Nat f g magicVoidO