| Portability | non-portable |
|---|---|
| Stability | experimental |
| Maintainer | sjoerd@w3future.com |
Data.Category.NaturalTransformation
Description
- 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
- data Nat where
- type Endo (~>) = Nat ~> ~>
- data FunctorCompose (~>) = FunctorCompose
- data Precompose where
- Precompose :: f -> Precompose f d
- data Postcompose where
- Postcompose :: f -> Postcompose f c
- data Wrap f h = Wrap f h
- type Presheaves (~>) = Nat (Op ~>) (->)
- class Functor f => Representable f where
- type RepresentingObject f :: *
- represent :: Dom f ~ Op c => f -> (c :-*: RepresentingObject f) :~> f
- unrepresent :: Dom f ~ Op c => f -> f :~> (c :-*: RepresentingObject f)
- data YonedaEmbedding where
- YonedaEmbedding :: Category ~> => YonedaEmbedding ~>
- data Yoneda f = Yoneda
- fromYoneda :: (Functor f, Cod f ~ (->)) => f -> Nat (Dom f) (->) (Yoneda f) f
- toYoneda :: (Functor f, Cod f ~ (->)) => f -> Nat (Dom f) (->) f (Yoneda f)
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.
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) | |
| (Category c, HasBinaryCoproducts d) => HasBinaryCoproducts (Nat c d) |
Related functors
data FunctorCompose (~>) Source
Composition of endofunctors is a functor.
Constructors
| FunctorCompose |
Instances
| Category ~> => Functor (FunctorCompose ~>) | |
| Category ~> => HasUnit (FunctorCompose ~>) | |
| Category ~> => TensorProduct (FunctorCompose ~>) |
data Precompose whereSource
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 :: f -> Precompose f d |
Instances
| (Functor f, Category d) => Functor (Precompose f d) |
data Postcompose whereSource
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 :: f -> Postcompose f c |
Instances
| (Functor f, Category c) => Functor (Postcompose f c) |
Wrap f h is the functor such that Wrap f h :% g = f :.: g :.: h,
for functors g that compose with f and h.
Constructors
| Wrap f h |
Presheaves
type Presheaves (~>) = Nat (Op ~>) (->)Source
class Functor f => Representable f whereSource
A functor F: Op(C) -> Set is representable if it is naturally isomorphic to the contravariant hom-functor.
Associated Types
type RepresentingObject f :: *Source
Methods
represent :: Dom f ~ Op c => f -> (c :-*: RepresentingObject f) :~> fSource
unrepresent :: Dom f ~ Op c => f -> f :~> (c :-*: RepresentingObject f)Source
Instances
| Category ~> => Representable (:-*: ~> x) |
Yoneda
data YonedaEmbedding whereSource
The Yoneda embedding functor.
Constructors
| YonedaEmbedding :: Category ~> => YonedaEmbedding ~> |
Instances
| Category ~> => Functor (YonedaEmbedding ~>) |