Portability | non-portable |
---|---|
Stability | experimental |
Maintainer | sjoerd@w3future.com |
- data Cat where
- data CatW
- type family Dom ftag :: * -> * -> *
- type family Cod ftag :: * -> * -> *
- class (Category (Dom ftag), Category (Cod ftag)) => 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 |
|
HasTerminalObject Cat |
|
HasInitialObject Cat | The empty category is the initial object in |
HasBinaryProducts Cat | |
HasBinaryCoproducts Cat | |
CartesianClosed 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.
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.