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.

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

(!) :: (Category c, Category d) => Nat c d f g -> c a b -> d (f :% a) (g :% b)

'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)

Horizontal composition of natural transformations.

natId :: Functor f => f -> Nat (Dom f) (Cod f) f f

The identity natural transformation of a functor.

srcF :: Nat c d f g -> f

tgtF :: Nat c d f g -> g

Functor category

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.

(Category c, HasTerminalObject d) => HasTerminalObject (Nat c d)

The constant functor to the terminal object is itself the terminal object in its functor category.

(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 c, HasBinaryProducts d) => HasBinaryProducts (Nat c d)

The functor product '(:*:)' is the binary product in functor categories.

(Category c, HasBinaryCoproducts d) => HasBinaryCoproducts (Nat c d)

The functor coproduct '(:+:)' is the binary coproduct in functor categories.

type Endo (~>) = Nat ~> ~>

The category of endofunctors.

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))

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)

Related functors

data FunctorCompose (~>)

Constructors

FunctorCompose

Instances

Category ~> => Functor (FunctorCompose ~>)

Composition of endofunctors is a functor.

Category ~> => TensorProduct (FunctorCompose ~>)

Functor composition makes the category of endofunctors monoidal, with the identity functor as unit.

data Precompose where

Constructors

Precompose :: f -> Precompose f d

Instances

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

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.

data Postcompose where

Constructors

Postcompose :: f -> Postcompose f c

Instances

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

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.

data Wrap f h

Constructors

Wrap f h

Instances

(Functor f, Functor h) => Functor (Wrap f h)

Wrap f h is the functor such that Wrap f h :% g = f :.: g :.: h, for functors g that compose with f and h.