| Portability | non-portable |
|---|---|
| Stability | experimental |
| Maintainer | sjoerd@w3future.com |
Data.Category.RepresentableFunctor
Description
- data Representable f repObj = Representable {
- representedFunctor :: f
- representingObject :: Obj (Dom f) repObj
- represent :: (Dom f ~ ~>, Cod f ~ (->)) => Obj ~> z -> (f :% z) -> repObj ~> z
- universalElement :: (Dom f ~ ~>, Cod f ~ (->)) => f :% repObj
- unrepresent :: (Functor f, Dom f ~ ~>, Cod f ~ (->)) => Representable f repObj -> (repObj ~> z) -> f :% z
- covariantHomRepr :: Category ~> => Obj ~> x -> Representable (x :*-: ~>) x
- contravariantHomRepr :: Category ~> => Obj ~> x -> Representable (~> :-*: x) x
- type InitialUniversal x u a = Representable ((x :*-: Cod u) :.: u) a
- initialUniversal :: Functor u => u -> Obj (Dom u) a -> Cod u x (u :% a) -> (forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y) -> InitialUniversal x u a
- type TerminalUniversal x u a = Representable ((Cod u :-*: x) :.: Opposite u) a
- terminalUniversal :: Functor u => u -> Obj (Dom u) a -> Cod u (u :% a) x -> (forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a) -> TerminalUniversal x u a
Documentation
data Representable f repObj Source
Constructors
| Representable | |
Fields
| |
unrepresent :: (Functor f, Dom f ~ ~>, Cod f ~ (->)) => Representable f repObj -> (repObj ~> z) -> f :% zSource
covariantHomRepr :: Category ~> => Obj ~> x -> Representable (x :*-: ~>) xSource
contravariantHomRepr :: Category ~> => Obj ~> x -> Representable (~> :-*: x) xSource
type InitialUniversal x u a = Representable ((x :*-: Cod u) :.: u) aSource
initialUniversal :: Functor u => u -> Obj (Dom u) a -> Cod u x (u :% a) -> (forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y) -> InitialUniversal x u aSource
An initial universal property, a universal morphism from x to u.
type TerminalUniversal x u a = Representable ((Cod u :-*: x) :.: Opposite u) aSource