module Data.Category.NaturalTransformation (
(:~>)
, Nat(..)
, Obj(..)
, Component
, Com(..)
, o
, (!)
, Precompose(..)
, Postcompose(..)
, YonedaEmbedding(..)
) where
import Prelude hiding ((.), id, Functor)
import Data.Category
import Data.Category.Functor
infixl 9 !
type f :~> g = (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Nat c d f g
data Nat :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where
Nat :: (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
type Component f g z = Cod f (f :% z) (g :% z)
instance (Category c, Category d) => Category (Nat c d) where
data Obj (Nat c d) a where
NatO :: (Functor f, Dom f ~ c, Cod f ~ d) => f -> Obj (Nat c d) f
src (Nat f _ _) = NatO f
tgt (Nat _ g _) = NatO g
id (NatO f) = Nat f f $ \i -> id $ f %% i
Nat _ h ngh . Nat f _ nfg = Nat f h $ \i -> ngh i . nfg i
o :: Category e => Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
Nat j k njk `o` Nat f g nfg = Nat (j :.: f) (k :.: g) $ \x -> k % nfg x . njk (f %% x)
newtype Com f g z = Com { unCom :: Component f g z }
(!) :: (Cod f ~ d, Cod g ~ d) => Nat (~>) d f g -> Obj (~>) a -> d (f :% a) (g :% a)
Nat _ _ n ! x = n x
data Precompose :: * -> (* -> * -> *) -> * where
Precompose :: (Functor f, Category d) => f -> Precompose f d
type instance Dom (Precompose f d) = Nat (Cod f) d
type instance Cod (Precompose f d) = Nat (Dom f) d
type instance Precompose f d :% g = g :.: f
instance Functor (Precompose f d) where
Precompose f %% NatO g = NatO $ g :.: f
Precompose f % (Nat g h n) = Nat (g :.: f) (h :.: f) $ n . (f %%)
data Postcompose :: * -> (* -> * -> *) -> * where
Postcompose :: (Functor f, Category c) => f -> Postcompose f c
type instance Dom (Postcompose f c) = Nat c (Dom f)
type instance Cod (Postcompose f c) = Nat c (Cod f)
type instance Postcompose f c :% g = f :.: g
instance Functor (Postcompose f c) where
Postcompose f %% NatO g = NatO $ f :.: g
Postcompose f % (Nat g h n) = Nat (f :.: g) (f :.: h) $ (f %) . n
class Functor f => Representable f where
type RepresentingObject f :: *
represent :: (Dom f ~ Op c) => f -> (c :-*: RepresentingObject f) :~> f
unrepresent :: (Dom f ~ Op c) => f -> f :~> (c :-*: RepresentingObject f)
instance Category (~>) => Representable ((~>) :-*: x) where
type RepresentingObject ((~>) :-*: x) = x
represent f = id $ NatO f
unrepresent f = id $ NatO f
data YonedaEmbedding :: (* -> * -> *) -> * where
YonedaEmbedding :: Category (~>) => YonedaEmbedding (~>)
type instance Dom (YonedaEmbedding (~>)) = (~>)
type instance Cod (YonedaEmbedding (~>)) = Nat (Op (~>)) (->)
type instance YonedaEmbedding (~>) :% a = (~>) :-*: a
instance Functor (YonedaEmbedding (~>)) where
YonedaEmbedding %% x = NatO $ Hom_X x
YonedaEmbedding % f = Nat (Hom_X $ src f) (Hom_X $ tgt f) $ \_ -> (f .)