Portability  nonportable 

Stability  experimental 
Maintainer  sjoerd@w3future.com 
Safe Haskell  SafeInferred 
 type :~> f g = (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Nat c d f g
 type Component f g z = Cod f (f :% z) (g :% z)
 newtype Com f g z = Com {}
 (!) :: (Category c, Category d) => Nat c d f g > c a b > d (f :% a) (g :% b)
 o :: (Category c, Category d, Category e) => Nat d e j k > Nat c d f g > Nat c e (j :.: f) (k :.: g)
 natId :: Functor f => f > Nat (Dom f) (Cod f) f f
 srcF :: Nat c d f g > f
 tgtF :: Nat c d f g > g
 data Nat where
 type Endo k = Nat k k
 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))
 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)
 idPrecomp :: Functor f => f > Nat (Dom f) (Cod f) (f :.: Id (Dom f)) f
 idPrecompInv :: Functor f => f > Nat (Dom f) (Cod f) f (f :.: Id (Dom f))
 idPostcomp :: Functor f => f > Nat (Dom f) (Cod f) (Id (Cod f) :.: f) f
 idPostcompInv :: Functor f => f > Nat (Dom f) (Cod f) f (Id (Cod 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))
 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)
 constPostcomp :: Functor f => Const (Cod f) c2 x > f > Nat (Dom f) c2 (Const (Cod f) c2 x :.: f) (Const (Dom f) c2 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)
 data FunctorCompose k = FunctorCompose
 data Precompose where
 Precompose :: f > Precompose f d
 data Postcompose where
 Postcompose :: f > Postcompose f c
 data Wrap f h = Wrap f h
Natural transformations
type :~> f g = (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Nat c d f gSource
f :~> g
is a natural transformation from functor f to functor g.
type Component f g z = Cod f (f :% z) (g :% z)Source
A component for an object z
is an arrow from F z
to G z
.
A newtype wrapper for components, which can be useful for helper functions dealing with components.
(!) :: (Category c, Category d) => Nat c d f g > c a b > d (f :% a) (g :% b)Source
'n ! a' returns the component for the object a
of a natural transformation n
.
This can be generalized to any arrow (instead of just identity arrows).
o :: (Category c, Category d, Category e) => Nat d e j k > Nat c d f g > Nat c e (j :.: f) (k :.: g)Source
Horizontal composition of natural transformations.
natId :: Functor f => f > Nat (Dom f) (Cod f) f fSource
The identity natural transformation of a functor.
Functor category
Natural transformations are built up of components,
one for each object z
in the domain category of f
and g
.
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 
(HasTerminalObject (Presheaves k), HasBinaryProducts (Presheaves k), Category k) => CartesianClosed (Presheaves k)  The category of presheaves on a category 
(Category c, Category d) => Category (Nat c d)  Functor category D^C. Objects of D^C are functors from C to D. Arrows of D^C are natural transformations. 
(Category (Nat c d), Category c, HasBinaryCoproducts d) => HasBinaryCoproducts (Nat c d)  The functor coproduct 
(Category (Nat c d), Category c, HasBinaryProducts d) => HasBinaryProducts (Nat c d)  The functor product 
(Category (Nat c d), Category c, HasInitialObject d) => HasInitialObject (Nat c d)  The constant functor to the initial object is itself the initial object in its functor category. 
(Category (Nat c d), Category c, HasTerminalObject d) => HasTerminalObject (Nat c d)  The constant functor to the terminal object is itself the terminal object in its functor category. 
Functor isomorphisms
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))Source
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)Source
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))Source
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)Source
constPostcomp :: Functor f => Const (Cod f) c2 x > f > Nat (Dom f) c2 (Const (Cod f) c2 x :.: f) (Const (Dom f) c2 x)Source
constPostcompInv :: Functor f => Const (Cod f) c2 x > f > Nat (Dom f) c2 (Const (Dom f) c2 x) (Const (Cod f) c2 x :.: f)Source
Related functors
data FunctorCompose k Source
(Category (Dom (FunctorCompose k)), Category (Cod (FunctorCompose k)), Category k) => Functor (FunctorCompose k)  Composition of endofunctors is a functor. 
(Functor (FunctorCompose k), ~ (* > * > *) (Dom (FunctorCompose k)) (:**: (Cod (FunctorCompose k)) (Cod (FunctorCompose k))), Category k) => TensorProduct (FunctorCompose k)  Functor composition makes the category of endofunctors monoidal, with the identity functor as unit. 
data Precompose whereSource
Precompose :: f > Precompose f d 
(Category (Dom (Precompose f d)), Category (Cod (Precompose f d)), Functor f, Category d) => Functor (Precompose f d) 

data Postcompose whereSource
Postcompose :: f > Postcompose f c 
(Category (Dom (Postcompose f c)), Category (Cod (Postcompose f c)), Functor f, Category c) => Functor (Postcompose f c) 
