Portability | non-portable |
---|---|
Stability | experimental |
Maintainer | sjoerd@w3future.com |
- data Cat where
- data CatW
- type family Dom ftag :: * -> * -> *
- type family Cod ftag :: * -> * -> *
- class Functor ftag where
- type family ftag :% a :: *
- data Id (~>) = Id
- data g :.: h where
- data Const c1 c2 x where
- type ConstF f = Const (Dom f) (Cod f)
- data :*-: where
- data :-*: where
- data Opposite f where
- data EndoHask where
- data InitialUniversal x u a = InitialUniversal {}
- data TerminalUniversal x u a = TerminalUniversal {}
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 |
|
HasBinaryProducts Cat | |
HasInitialObject Cat | |
HasTerminalObject Cat |
|
We need a wrapper here because objects need to be of kind *, and categories are of kind * -> * -> *.
Functors
class Functor ftag whereSource
Functors map objects and arrows. As objects are represented at both the type and value level, we need 3 maps in total.
(%%) :: ftag -> Obj (Dom ftag) a -> Obj (Cod ftag) (ftag :% a)Source
%%
maps objects at the value level.
(%) :: ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)Source
%
maps arrows.
Functor (EndoHask f) | |
Functor (Opposite f) | |
Functor (Id ~>) | |
Functor (YonedaEmbedding ~>) | |
Functor (VoidDiagram ~>) | |
Functor (DiagProd ~>) | |
Functor (Hom ~>) | |
Functor (NatF ~>) | |
Functor (:-*: ~> x) | |
Functor (:*-: x ~>) | |
Functor (:.: g h) | |
Functor (Postcompose f c) | |
Functor (Precompose f d) | |
Functor (:***: f1 f2) | |
Functor (Proj2 c1 c2) | |
Functor (Proj1 c1 c2) | |
Functor (Next n f) | |
Functor (ColimitFunctor j ~>) | |
Functor (LimitFunctor j ~>) | |
Functor (Diag j ~>) | |
Functor (KleisliAdjG ~> m) | |
Functor (KleisliAdjF ~> m) | |
Functor (Const c1 c2 x) | |
Functor (PairDiagram ~> x y) | |
Functor (DiscreteDiagram ~> n xs) |
Functor instances
The identity functor on (~>)
The composition of two functors.
The covariant functor Hom(X,--)
The contravariant functor Hom(--,X)
The dual of a functor
Universal properties
data InitialUniversal x u a Source
An initial universal property, a universal morphism from x to u.
data TerminalUniversal x u a Source
A terminal universal property, a universal morphism from u to x.