{-# LANGUAGE EmptyCase, LambdaCase, TypeOperators, GADTs, TypeFamilies, NoImplicitPrelude #-}
module Data.Category.Void where
import Data.Category
import Data.Category.Functor
import Data.Category.NaturalTransformation
data Void a b
magic :: Void a b -> x
magic :: Void a b -> x
magic = \case { }
instance Category Void where
src :: Void a b -> Obj Void a
src = Void a b -> Obj Void a
forall a b x. Void a b -> x
magic
tgt :: Void a b -> Obj Void b
tgt = Void a b -> Obj Void b
forall a b x. Void a b -> x
magic
. :: Void b c -> Void a b -> Void a c
(.) = Void b c -> Void a b -> Void a c
forall a b x. Void a b -> x
magic
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 Void d f g
voidNat f
f g
g = f
-> g -> (forall z. Obj Void z -> Component f g z) -> Nat Void d f g
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat f
f g
g forall z. Obj Void z -> Component f g z
forall a b x. Void a b -> x
magic
data Magic (k :: * -> * -> *) = Magic
instance Category k => Functor (Magic k) where
type Dom (Magic k) = Void
type Cod (Magic k) = k
Magic k
Magic % :: Magic k
-> Dom (Magic k) a b -> Cod (Magic k) (Magic k :% a) (Magic k :% b)
% Dom (Magic k) a b
f = Void a b -> k (Magic k :% a) (Magic k :% b)
forall a b x. Void a b -> x
magic Dom (Magic k) a b
Void a b
f