Data.Category.NaturalTransformation

Natural transformations

type :~> f g = (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Nat c d f g

f :~> g is a natural transformation from functor f to functor g.

data Nat where

Natural transformations are built up of components, one for each object z in the domain category of f and g.

Constructors

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

Instances

(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.

type Component f g z = Cod f (f :% z) (g :% z)

A component for an object z is an arrow from F z to G z.

newtype Com f g z

A newtype wrapper for components, which can be useful for helper functions dealing with components.

Constructors

Com

Fields

unCom :: Component f g z

o :: Category e => Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)

Horizontal composition of natural transformations.

(!) :: (Cod f ~ d, Cod g ~ d) => Nat ~> d f g -> Obj ~> a -> d (f :% a) (g :% a)

'n ! a' returns the component for the object a of a natural transformation n.

Related functors

data Precompose where

Precompose f d is the functor such that Precompose f d :% g = g :.: f, for functors g that compose with f and with codomain d.

Constructors

Precompose :: (Functor f, Category d) => f -> Precompose f d

Instances

Functor (Precompose f d)

data Postcompose where

Postcompose f c is the functor such that Postcompose f c :% g = f :.: g, for functors g that compose with f and with domain c.

Constructors

Postcompose :: (Functor f, Category c) => f -> Postcompose f c

Instances

Functor (Postcompose f c)

data YonedaEmbedding where

The Yoneda embedding functor.

Constructors

YonedaEmbedding :: Category ~> => YonedaEmbedding ~>

Instances

Functor (YonedaEmbedding ~>)