License | BSD-style (see the file LICENSE) |
---|---|
Maintainer | sjoerd@w3future.com |
Stability | experimental |
Portability | non-portable |
Safe Haskell | Safe |
Language | Haskell2010 |
- type (:~>) f g = forall c d. (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
- type Presheaves k = Nat (Op 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 :: (Category c2, Functor f) => Const (Cod f) c2 x -> f -> Nat (Dom f) c2 (Const (Cod f) c2 x :.: f) (Const (Dom f) c2 x)
- constPostcompInv :: (Category c2, 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 c d e = FunctorCompose
- type EndoFunctorCompose k = FunctorCompose k k k
- type Precompose f e = FunctorCompose (Dom f) (Cod f) e :.: Tuple2 (Nat (Cod f) e) (Nat (Dom f) (Cod f)) f
- 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 :: (Category e, Functor f) => f -> Postcompose f e
- data Wrap f h = Wrap f h
- data Apply c1 c2 = Apply
- data Tuple c1 c2 = Tuple
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 Source #
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) infixl 9 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 f Source #
The identity natural transformation of a functor.
Functor category
data Nat :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where Source #
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 |
Category k => CartesianClosed (Presheaves k) Source # | The category of presheaves on a category |
Category d => Category (Nat c d) Source # | Functor category D^C. Objects of D^C are functors from C to D. Arrows of D^C are natural transformations. |
(Category c, HasBinaryCoproducts d) => HasBinaryCoproducts (Nat c d) Source # | The functor coproduct |
(Category c, HasBinaryProducts d) => HasBinaryProducts (Nat c d) Source # | The functor product |
(Category c, HasInitialObject d) => HasInitialObject (Nat c d) Source # | The constant functor to the initial object is itself the initial object in its functor category. |
(Category c, HasTerminalObject d) => HasTerminalObject (Nat c d) Source # | The constant functor to the terminal object is itself the terminal object in its functor category. |
type Exponential (Presheaves k) y z Source # | |
type InitialObject (Nat c d) Source # | |
type TerminalObject (Nat c d) Source # | |
type BinaryCoproduct (Nat c d) x y Source # | |
type BinaryProduct (Nat c d) x y Source # | |
type Presheaves k = Nat (Op k) (->) Source #
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 :: (Category c2, 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 :: (Category c2, 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 c d e Source #
Category k => TensorProduct (EndoFunctorCompose k) Source # | Functor composition makes the category of endofunctors monoidal, with the identity functor as unit. |
(Category c, Category d, Category e) => Functor (FunctorCompose c d e) Source # | Composition of functors is a functor. |
type Unit (EndoFunctorCompose k) Source # | |
type Dom (FunctorCompose c d e) Source # | |
type Cod (FunctorCompose c d e) Source # | |
type (FunctorCompose c d e) :% (f, g) Source # | |
type EndoFunctorCompose k = FunctorCompose k k k Source #
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 Source #
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
.
precompose :: (Category e, Functor f) => f -> Precompose f e Source #
type Postcompose f c = FunctorCompose c (Dom f) (Cod f) :.: Tuple1 (Nat (Dom f) (Cod f)) (Nat c (Dom f)) f Source #
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
.
postcompose :: (Category e, Functor f) => f -> Postcompose f e Source #
Wrap f h |