Portability | non-portable |
---|---|
Stability | experimental |
Maintainer | sjoerd@w3future.com |
Safe Haskell | Safe-Inferred |
- data Cat where
- data CatW
- class (Category (Dom ftag), Category (Cod ftag)) => Functor ftag where
- data Id k = Id
- data g :.: h where
- data Const c1 c2 x where
- type ConstF f = Const (Dom f) (Cod f)
- data Opposite f where
- data OpOp k = OpOp
- data OpOpInv k = OpOpInv
- data Proj1 c1 c2 = Proj1
- data Proj2 c1 c2 = Proj2
- data f1 :***: f2 = f1 :***: f2
- data DiagProd k = DiagProd
- data Tuple1 c1 c2 a = Tuple1 (Obj c1 a)
- data Tuple2 c1 c2 a = Tuple2 (Obj c2 a)
- data Hom k = Hom
- type :*-: x k = Hom k :.: Tuple1 (Op k) k x
- homX_ :: Category k => Obj k x -> x :*-: k
- type :-*: k x = Hom k :.: Tuple2 (Op k) k x
- hom_X :: Category k => Obj k x -> k :-*: x
Cat
Functors are arrows in the category Cat.
CatA :: (Functor ftag, Category (Dom ftag), Category (Cod ftag)) => ftag -> Cat (CatW (Dom ftag)) (CatW (Cod ftag)) |
Category Cat |
|
HasBinaryCoproducts Cat | The coproduct of categories |
HasBinaryProducts Cat | The product of categories |
HasInitialObject Cat | The empty category is the initial object in |
HasTerminalObject Cat |
|
CartesianClosed Cat | Exponentials in |
HasNaturalNumberObject Cat |
We need a wrapper here because objects need to be of kind *, and categories are of kind * -> * -> *.
Functors
class (Category (Dom ftag), Category (Cod ftag)) => Functor ftag whereSource
Functors map objects and arrows.
type Dom ftag :: * -> * -> *Source
The domain, or source category, of the functor.
type Cod ftag :: * -> * -> *Source
The codomain, or target category, of the functor.
:%
maps objects.
Functor Add | Ordinal addition is a bifuntor, it concattenates the maps as it were. |
Functor Forget | Turn |
(Category (Dom (Hom k)), Category (Cod (Hom k)), Category k) => Functor (Hom k) | The Hom functor, Hom(--,--), a bifunctor contravariant in its first argument and covariant in its second argument. |
(Category (Dom (DiagProd k)), Category (Cod (DiagProd k)), Category k) => Functor (DiagProd k) |
|
(Category (Dom (OpOpInv k)), Category (Cod (OpOpInv k)), Category k) => Functor (OpOpInv k) | The |
(Category (Dom (OpOp k)), Category (Cod (OpOp k)), Category k) => Functor (OpOp k) | The |
(Category (Dom (Opposite f)), Category (Cod (Opposite f)), Category (Dom f), Category (Cod f)) => Functor (Opposite f) | The dual of a functor |
(Category (Dom (Id k)), Category (Cod (Id k)), Category k) => Functor (Id k) | The identity functor on k |
(Category (Dom (FunctorCompose k)), Category (Cod (FunctorCompose k)), Category k) => Functor (FunctorCompose k) | Composition of endofunctors is a functor. |
(Category (Dom (Magic k)), Category (Cod (Magic k)), Category k) => Functor (Magic k) | Since there is nothing to map in |
(Category (Dom (CodiagCoprod k)), Category (Cod (CodiagCoprod k)), Category k) => Functor (CodiagCoprod k) |
|
(Category (Dom (CoproductFunctor k)), Category (Cod (CoproductFunctor k)), HasBinaryCoproducts k) => Functor (CoproductFunctor k) | Binary coproduct as a bifunctor. |
(Category (Dom (ProductFunctor k)), Category (Cod (ProductFunctor k)), HasBinaryProducts k) => Functor (ProductFunctor k) | Binary product as a bifunctor. |
(Category (Dom (ExpFunctor k)), Category (Cod (ExpFunctor k)), CartesianClosed k) => Functor (ExpFunctor k) | The exponential as a bifunctor. |
(Category (Dom (Wrap f)), Category (Cod (Wrap f)), Category (f (Fix f))) => Functor (Wrap f) | |
(Category (Dom (KleisliAdjG m)), Category (Cod (KleisliAdjG m)), Functor m, ~ (* -> * -> *) (Dom m) k, ~ (* -> * -> *) (Cod m) k) => Functor (KleisliAdjG m) | |
(Category (Dom (KleisliAdjF m)), Category (Cod (KleisliAdjF m)), Functor m, ~ (* -> * -> *) (Dom m) k, ~ (* -> * -> *) (Cod m) k) => Functor (KleisliAdjF m) | |
(Category (Dom (ForgetAlg m)), Category (Cod (ForgetAlg m)), Functor m, ~ (* -> * -> *) (Dom m) k, ~ (* -> * -> *) (Cod m) k) => Functor (ForgetAlg m) |
|
(Category (Dom (FreeAlg m)), Category (Cod (FreeAlg m)), Functor m, ~ (* -> * -> *) (Dom m) k, ~ (* -> * -> *) (Cod m) k) => Functor (FreeAlg m) |
|
(Category (Dom (:***: f1 f2)), Category (Cod (:***: f1 f2)), Functor f1, Functor f2) => Functor (:***: f1 f2) |
|
(Category (Dom (Proj2 c1 c2)), Category (Cod (Proj2 c1 c2)), Category c1, Category c2) => Functor (Proj2 c1 c2) |
|
(Category (Dom (Proj1 c1 c2)), Category (Cod (Proj1 c1 c2)), Category c1, Category c2) => Functor (Proj1 c1 c2) |
|
(Category (Dom (:.: g h)), Category (Cod (:.: g h)), Category (Cod g), Category (Dom h)) => Functor (:.: g h) | The composition of two functors. |
(Category (Dom (Wrap f h)), Category (Cod (Wrap f h)), Functor f, Functor h) => Functor (Wrap f h) |
|
(Category (Dom (Postcompose f c)), Category (Cod (Postcompose f c)), Functor f, Category c) => Functor (Postcompose f c) |
|
(Category (Dom (Precompose f d)), Category (Cod (Precompose f d)), Functor f, Category d) => Functor (Precompose f d) |
|
(Category (Dom (NatAsFunctor f g)), Category (Cod (NatAsFunctor f g)), Functor f, Functor g, ~ (* -> * -> *) (Dom f) (Dom g), ~ (* -> * -> *) (Cod f) (Cod g)) => Functor (NatAsFunctor f g) | A natural transformation |
(Category (Dom (:+++: f1 f2)), Category (Cod (:+++: f1 f2)), Functor f1, Functor f2) => Functor (:+++: f1 f2) |
|
(Category (Dom (Inj2 c1 c2)), Category (Cod (Inj2 c1 c2)), Category c1, Category c2) => Functor (Inj2 c1 c2) |
|
(Category (Dom (Inj1 c1 c2)), Category (Cod (Inj1 c1 c2)), Category c1, Category c2) => Functor (Inj1 c1 c2) |
|
(Category (Dom (:+: p q)), Category (Cod (:+: p q)), Category (Dom p), Category (Cod p)) => Functor (:+: p q) | The coproduct of two functors, passing the same object to both functors and taking the coproduct of the results. |
(Category (Dom (:*: p q)), Category (Cod (:*: p q)), Category (Dom p), Category (Cod p)) => Functor (:*: p q) | The product of two functors, passing the same object to both functors and taking the product of the results. |
(Category (Dom (ColimitFunctor j k)), Category (Cod (ColimitFunctor j k)), HasColimits j k) => Functor (ColimitFunctor j k) | If every diagram of type |
(Category (Dom (LimitFunctor j k)), Category (Cod (LimitFunctor j k)), HasLimits j k) => Functor (LimitFunctor j k) | If every diagram of type |
(Category (Dom (Diag j k)), Category (Cod (Diag j k)), Category j, Category k) => Functor (Diag j k) | The diagonal functor from (index-) category J to k. |
(Category (Dom (ToTuple2 y z)), Category (Cod (ToTuple2 y z)), Category y, Category z) => Functor (ToTuple2 y z) | |
(Category (Dom (ToTuple1 y z)), Category (Cod (ToTuple1 y z)), Category y, Category z) => Functor (ToTuple1 y z) | |
(Category (Dom (Apply y z)), Category (Cod (Apply y z)), Category y, Category z) => Functor (Apply y z) |
|
(Category (Dom (Yoneda k f)), Category (Cod (Yoneda k f)), Category k, Functor f, ~ (* -> * -> *) (Dom f) (Op k), ~ (* -> * -> *) (Cod f) (->)) => Functor (Yoneda k f) |
|
(Category (Dom (PrimRec z s)), Category (Cod (PrimRec z s)), Functor z, Functor s, ~ (* -> * -> *) (Dom z) Unit, ~ (* -> * -> *) (Cod z) (Dom s), ~ (* -> * -> *) (Dom s) (Cod s)) => Functor (PrimRec z s) | |
(Category (Dom (Replicate f a)), Category (Cod (Replicate f a)), TensorProduct f) => Functor (Replicate f a) | Replicate a monoid a number of times. |
(Category (Dom (Tuple2 c1 c2 a2)), Category (Cod (Tuple2 c1 c2 a2)), Category c1, Category c2) => Functor (Tuple2 c1 c2 a2) |
|
(Category (Dom (Tuple1 c1 c2 a1)), Category (Cod (Tuple1 c1 c2 a1)), Category c1, Category c2) => Functor (Tuple1 c1 c2 a1) |
|
(Category (Dom (Const c1 c2 x)), Category (Cod (Const c1 c2 x)), Category c1, Category c2) => Functor (Const c1 c2 x) | The constant functor. |
(Category (Dom (Cotuple2 c1 c2 a2)), Category (Cod (Cotuple2 c1 c2 a2)), Category c1, Category c2) => Functor (Cotuple2 c1 c2 a2) |
|
(Category (Dom (Cotuple1 c1 c2 a1)), Category (Cod (Cotuple1 c1 c2 a1)), Category c1, Category c2) => Functor (Cotuple1 c1 c2 a1) |
|
Functor instances
type ConstF f = Const (Dom f) (Cod f)Source
The constant functor with the same domain and codomain as f.
Related to the product category
f1 :***: f2 |
(Category (Dom (DiagProd k)), Category (Cod (DiagProd k)), Category k) => Functor (DiagProd k) |
|
HasInitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) | The category for defining the natural numbers and primitive recursion can be described as
|
HasInitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) | The category for defining the natural numbers and primitive recursion can be described as
|
(Category (Dom (Tuple1 c1 c2 a1)), Category (Cod (Tuple1 c1 c2 a1)), Category c1, Category c2) => Functor (Tuple1 c1 c2 a1) |
|