module Data.Category.NaturalTransformation (
(:~>)
, Component
, Com(..)
, (!)
, o
, natId
, srcF
, tgtF
, Nat(..)
, Endo
, compAssoc
, compAssocInv
, idPrecomp
, idPrecompInv
, idPostcomp
, idPostcompInv
, constPrecomp
, constPrecompInv
, constPostcomp
, constPostcompInv
, FunctorCompose(..)
, Precompose(..)
, Postcompose(..)
, Wrap(..)
) where
import Prelude hiding ((.), Functor)
import Data.Category
import Data.Category.Functor
import Data.Category.Product
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)
newtype Com f g z = Com { unCom :: Component f g z }
(!) :: (Category c, Category d) => Nat c d f g -> c a b -> d (f :% a) (g :% b)
Nat f _ n ! h = n (tgt h) . f % h
o :: (Category c, Category d, Category e) => Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
njk@(Nat j k _) `o` nfg@(Nat f g _) = Nat (j :.: f) (k :.: g) $ (njk !) . (nfg !)
natId :: Functor f => f -> Nat (Dom f) (Cod f) f f
natId f = Nat f f $ \i -> f % i
srcF :: Nat c d f g -> f
srcF (Nat f _ _) = f
tgtF :: Nat c d f g -> g
tgtF (Nat _ g _) = g
instance (Category c, Category d) => Category (Nat c d) where
src (Nat f _ _) = natId f
tgt (Nat _ g _) = natId g
Nat _ h ngh . Nat f _ nfg = Nat f h $ \i -> ngh i . nfg i
compAssoc :: (Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h)
=> f -> g -> h -> Nat (Dom h) (Cod f) ((f :.: g) :.: h) (f :.: (g :.: h))
compAssoc f g h = Nat ((f :.: g) :.: h) (f :.: (g :.: h)) $ \i -> f % g % h % i
compAssocInv :: (Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h)
=> f -> g -> h -> Nat (Dom h) (Cod f) (f :.: (g :.: h)) ((f :.: g) :.: h)
compAssocInv f g h = Nat (f :.: (g :.: h)) ((f :.: g) :.: h) $ \i -> f % g % h % i
idPrecomp :: Functor f => f -> Nat (Dom f) (Cod f) (f :.: Id (Dom f)) f
idPrecomp f = Nat (f :.: Id) f (f %)
idPrecompInv :: Functor f => f -> Nat (Dom f) (Cod f) f (f :.: Id (Dom f))
idPrecompInv f = Nat f (f :.: Id) (f %)
idPostcomp :: Functor f => f -> Nat (Dom f) (Cod f) (Id (Cod f) :.: f) f
idPostcomp f = Nat (Id :.: f) f (f %)
idPostcompInv :: Functor f => f -> Nat (Dom f) (Cod f) f (Id (Cod f) :.: f)
idPostcompInv f = Nat f (Id :.: f) (f %)
constPrecomp :: (Category c1, Functor f) => Const c1 (Dom f) x -> f -> Nat c1 (Cod f) (f :.: Const c1 (Dom f) x) (Const c1 (Cod f) (f :% x))
constPrecomp (Const x) f = let fx = f % x in Nat (f :.: Const x) (Const fx) $ const fx
constPrecompInv :: (Category c1, Functor f) => Const c1 (Dom f) x -> f -> Nat c1 (Cod f) (Const c1 (Cod f) (f :% x)) (f :.: Const c1 (Dom f) x)
constPrecompInv (Const x) f = let fx = f % x in Nat (Const fx) (f :.: Const x) $ const fx
constPostcomp :: Functor f => Const (Cod f) c2 x -> f -> Nat (Dom f) c2 (Const (Cod f) c2 x :.: f) (Const (Dom f) c2 x)
constPostcomp (Const x) f = Nat (Const x :.: f) (Const x) $ const x
constPostcompInv :: Functor f => Const (Cod f) c2 x -> f -> Nat (Dom f) c2 (Const (Dom f) c2 x) (Const (Cod f) c2 x :.: f)
constPostcompInv (Const x) f = Nat (Const x) (Const x :.: f) $ const x
type Endo (~>) = Nat (~>) (~>)
data FunctorCompose ((~>) :: * -> * -> *) = FunctorCompose
type instance Dom (FunctorCompose (~>)) = Endo (~>) :**: Endo (~>)
type instance Cod (FunctorCompose (~>)) = Endo (~>)
type instance FunctorCompose (~>) :% (f, g) = f :.: g
instance Category (~>) => Functor (FunctorCompose (~>)) where
FunctorCompose % (n1 :**: n2) = n1 `o` n2
data Precompose :: * -> (* -> * -> *) -> * where
Precompose :: 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 f, Category d) => Functor (Precompose f d) where
Precompose f % n = n `o` natId f
data Postcompose :: * -> (* -> * -> *) -> * where
Postcompose :: 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 f, Category c) => Functor (Postcompose f c) where
Postcompose f % n = natId f `o` n
data Wrap f h = Wrap f h
type instance Dom (Wrap f h) = Nat (Cod h) (Dom f)
type instance Cod (Wrap f h) = Nat (Dom h) (Cod f)
type instance Wrap f h :% g = f :.: g :.: h
instance (Functor f, Functor h) => Functor (Wrap f h) where
Wrap f h % n = natId f `o` n `o` natId h