Data.Category.NaturalTransformation

Natural transformations

type (:~>) f g = forall c d. (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.

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

'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 k => CartesianClosed (Presheaves k)

The category of presheaves on a category C is cartesian closed for any C.

Defined in Data.Category.CartesianClosed

Associated Types

type Exponential (Presheaves k) y z :: Type

Methods

apply :: Obj (Presheaves k) y -> Obj (Presheaves k) z -> Presheaves k (BinaryProduct (Presheaves k) (Exponential (Presheaves k) y z) y) z

tuple :: Obj (Presheaves k) y -> Obj (Presheaves k) z -> Presheaves k z (Exponential (Presheaves k) y (BinaryProduct (Presheaves k) z y))

(^^^) :: Presheaves k z1 z2 -> Presheaves k y2 y1 -> Presheaves k (Exponential (Presheaves k) y1 z1) (Exponential (Presheaves k) y2 z2)

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.

Defined in Data.Category.NaturalTransformation

Methods

src :: Nat c d a b -> Obj (Nat c d) a

tgt :: Nat c d a b -> Obj (Nat c d) b

(.) :: Nat c d b c0 -> Nat c d a b -> Nat c d a c0

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

The functor coproduct :+: is the binary coproduct in functor categories.

Defined in Data.Category.Limit

Associated Types

type BinaryCoproduct (Nat c d) x y :: Type

Methods

inj1 :: Obj (Nat c d) x -> Obj (Nat c d) y -> Nat c d x (BinaryCoproduct (Nat c d) x y)

inj2 :: Obj (Nat c d) x -> Obj (Nat c d) y -> Nat c d y (BinaryCoproduct (Nat c d) x y)

(|||) :: Nat c d x a -> Nat c d y a -> Nat c d (BinaryCoproduct (Nat c d) x y) a

(+++) :: Nat c d a1 b1 -> Nat c d a2 b2 -> Nat c d (BinaryCoproduct (Nat c d) a1 a2) (BinaryCoproduct (Nat c d) b1 b2)

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

The functor product :*: is the binary product in functor categories.

Defined in Data.Category.Limit

Associated Types

type BinaryProduct (Nat c d) x y :: Type

Methods

proj1 :: Obj (Nat c d) x -> Obj (Nat c d) y -> Nat c d (BinaryProduct (Nat c d) x y) x

proj2 :: Obj (Nat c d) x -> Obj (Nat c d) y -> Nat c d (BinaryProduct (Nat c d) x y) y

(&&&) :: Nat c d a x -> Nat c d a y -> Nat c d a (BinaryProduct (Nat c d) x y)

(***) :: Nat c d a1 b1 -> Nat c d a2 b2 -> Nat c d (BinaryProduct (Nat c d) a1 a2) (BinaryProduct (Nat c d) b1 b2)

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

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

Defined in Data.Category.Limit

Associated Types

type InitialObject (Nat c d) :: Type

Methods

initialObject :: Obj (Nat c d) (InitialObject (Nat c d))

initialize :: Obj (Nat c d) a -> Nat c d (InitialObject (Nat c d)) a

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

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

Defined in Data.Category.Limit

Associated Types

type TerminalObject (Nat c d) :: Type

Methods

terminalObject :: Obj (Nat c d) (TerminalObject (Nat c d))

terminate :: Obj (Nat c d) a -> Nat c d a (TerminalObject (Nat c d))

type Exponential (Presheaves k) y z

Defined in Data.Category.CartesianClosed

type Exponential (Presheaves k) y z = PShExponential k y z

type InitialObject (Nat c d)

Defined in Data.Category.Limit

type InitialObject (Nat c d) = Const c d (InitialObject d)

type TerminalObject (Nat c d)

Defined in Data.Category.Limit

type TerminalObject (Nat c d) = Const c d (TerminalObject d)

type BinaryCoproduct (Nat c d) x y

Defined in Data.Category.Limit

type BinaryCoproduct (Nat c d) x y = x :+: y

type BinaryProduct (Nat c d) x y

Defined in Data.Category.Limit

type BinaryProduct (Nat c d) x y = x :*: y

type Endo k = Nat k k

The category of endofunctors.

type Presheaves k = Nat (Op k) (->)

type Profunctors c d = Nat (Op d :**: c) (->)

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)

constPrecompIn :: Nat j d (f :.: Const j c x) g -> Nat j d (Const j d (f :% x)) g

constPrecompOut :: Nat j d f (g :.: Const j c x) -> Nat j d f (Const j d (g :% x))

constPostcompIn :: Nat j d (Const k d x :.: f) g -> Nat j d (Const j d x) g

constPostcompOut :: Nat j d f (Const k d x :.: g) -> Nat j d f (Const j d x)

Related functors

data FunctorCompose (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *)

Constructors

FunctorCompose

Instances

Category k => TensorProduct (EndoFunctorCompose k)

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

Defined in Data.Category.Monoidal

Associated Types

type Unit (EndoFunctorCompose k) :: Type

Methods

unitObject :: EndoFunctorCompose k -> Obj (Cod (EndoFunctorCompose k)) (Unit (EndoFunctorCompose k))

leftUnitor :: Cod (EndoFunctorCompose k) ~ k0 => EndoFunctorCompose k -> Obj k0 a -> k0 (EndoFunctorCompose k :% (Unit (EndoFunctorCompose k), a)) a

leftUnitorInv :: Cod (EndoFunctorCompose k) ~ k0 => EndoFunctorCompose k -> Obj k0 a -> k0 a (EndoFunctorCompose k :% (Unit (EndoFunctorCompose k), a))

rightUnitor :: Cod (EndoFunctorCompose k) ~ k0 => EndoFunctorCompose k -> Obj k0 a -> k0 (EndoFunctorCompose k :% (a, Unit (EndoFunctorCompose k))) a

rightUnitorInv :: Cod (EndoFunctorCompose k) ~ k0 => EndoFunctorCompose k -> Obj k0 a -> k0 a (EndoFunctorCompose k :% (a, Unit (EndoFunctorCompose k)))

associator :: Cod (EndoFunctorCompose k) ~ k0 => EndoFunctorCompose k -> Obj k0 a -> Obj k0 b -> Obj k0 c -> k0 (EndoFunctorCompose k :% (EndoFunctorCompose k :% (a, b), c)) (EndoFunctorCompose k :% (a, EndoFunctorCompose k :% (b, c)))

associatorInv :: Cod (EndoFunctorCompose k) ~ k0 => EndoFunctorCompose k -> Obj k0 a -> Obj k0 b -> Obj k0 c -> k0 (EndoFunctorCompose k :% (a, EndoFunctorCompose k :% (b, c))) (EndoFunctorCompose k :% (EndoFunctorCompose k :% (a, b), c))

(Category c, Category d, Category e) => Functor (FunctorCompose c d e)

Composition of functors is a functor.

Defined in Data.Category.NaturalTransformation

Associated Types

type Dom (FunctorCompose c d e) :: Type -> Type -> Type

type Cod (FunctorCompose c d e) :: Type -> Type -> Type

type (FunctorCompose c d e) :% a :: Type

Methods

(%) :: FunctorCompose c d e -> Dom (FunctorCompose c d e) a b -> Cod (FunctorCompose c d e) (FunctorCompose c d e :% a) (FunctorCompose c d e :% b)

type Unit (EndoFunctorCompose k)

Defined in Data.Category.Monoidal

type Unit (EndoFunctorCompose k) = Id k

type Dom (FunctorCompose c d e)

Defined in Data.Category.NaturalTransformation

type Dom (FunctorCompose c d e) = Nat d e :**: Nat c d

type Cod (FunctorCompose c d e)

Defined in Data.Category.NaturalTransformation

type Cod (FunctorCompose c d e) = Nat c e

type (FunctorCompose c d e) :% (f, g)

Defined in Data.Category.NaturalTransformation

type (FunctorCompose c d e) :% (f, g) = f :.: g

type EndoFunctorCompose k = FunctorCompose k k k

Composition of endofunctors is a functor.

type Precompose f e = FunctorCompose (Dom f) (Cod f) e :.: Tuple2 (Nat (Cod f) e) (Nat (Dom f) (Cod f)) f

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

pattern Precompose :: (Category e, Functor f) => f -> Precompose f e

type Postcompose f c = FunctorCompose c (Dom f) (Cod f) :.: Tuple1 (Nat (Dom f) (Cod f)) (Nat c (Dom f)) f

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.

pattern Postcompose :: (Category e, Functor f) => f -> Postcompose f e

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.

Defined in Data.Category.NaturalTransformation

Associated Types

type Dom (Wrap f h) :: Type -> Type -> Type

type Cod (Wrap f h) :: Type -> Type -> Type

type (Wrap f h) :% a :: Type

Methods

(%) :: Wrap f h -> Dom (Wrap f h) a b -> Cod (Wrap f h) (Wrap f h :% a) (Wrap f h :% b)

type Dom (Wrap f h)

Defined in Data.Category.NaturalTransformation

type Dom (Wrap f h) = Nat (Cod h) (Dom f)

type Cod (Wrap f h)

Defined in Data.Category.NaturalTransformation

type Cod (Wrap f h) = Nat (Dom h) (Cod f)

type (Wrap f h) :% g

Defined in Data.Category.NaturalTransformation

type (Wrap f h) :% g = (f :.: g) :.: h

data Apply (c1 :: * -> * -> *) (c2 :: * -> * -> *)

Constructors

Apply

Instances

(Category c1, Category c2) => Functor (Apply c1 c2)

Apply is a bifunctor, Apply :% (f, a) applies f to a, i.e. f :% a.

Defined in Data.Category.NaturalTransformation

Associated Types

type Dom (Apply c1 c2) :: Type -> Type -> Type

type Cod (Apply c1 c2) :: Type -> Type -> Type

type (Apply c1 c2) :% a :: Type

Methods

(%) :: Apply c1 c2 -> Dom (Apply c1 c2) a b -> Cod (Apply c1 c2) (Apply c1 c2 :% a) (Apply c1 c2 :% b)

type Dom (Apply c1 c2)

Defined in Data.Category.NaturalTransformation

type Dom (Apply c1 c2) = Nat c2 c1 :**: c2

type Cod (Apply c1 c2)

Defined in Data.Category.NaturalTransformation

type Cod (Apply c1 c2) = c1

type (Apply c1 c2) :% (f, a)

Defined in Data.Category.NaturalTransformation

type (Apply c1 c2) :% (f, a) = f :% a

data Tuple (c1 :: * -> * -> *) (c2 :: * -> * -> *)

Constructors

Tuple

Instances

(Category c1, Category c2) => Functor (Tuple c1 c2)

Tuple converts an object a to the functor Tuple1 a.

Defined in Data.Category.NaturalTransformation

Associated Types

type Dom (Tuple c1 c2) :: Type -> Type -> Type

type Cod (Tuple c1 c2) :: Type -> Type -> Type

type (Tuple c1 c2) :% a :: Type

Methods

(%) :: Tuple c1 c2 -> Dom (Tuple c1 c2) a b -> Cod (Tuple c1 c2) (Tuple c1 c2 :% a) (Tuple c1 c2 :% b)

type Dom (Tuple c1 c2)

Defined in Data.Category.NaturalTransformation

type Dom (Tuple c1 c2) = c1

type Cod (Tuple c1 c2)

Defined in Data.Category.NaturalTransformation

type Cod (Tuple c1 c2) = Nat c2 (c1 :**: c2)

type (Tuple c1 c2) :% a

Defined in Data.Category.NaturalTransformation

type (Tuple c1 c2) :% a = Tuple1 c1 c2 a