| License | BSD-style (see the file LICENSE) |
|---|---|
| Maintainer | sjoerd@w3future.com |
| Stability | experimental |
| Portability | non-portable |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Data.Category.RepresentableFunctor
Description
Synopsis
- data Representable f repObj = Representable {
- representedFunctor :: f
- representingObject :: Obj (Dom f) repObj
- represent :: forall k z. (Dom f ~ k, Cod f ~ (->)) => Obj k z -> (f :% z) -> k repObj z
- universalElement :: forall k. (Dom f ~ k, Cod f ~ (->)) => f :% repObj
- unrepresent :: (Functor f, Dom f ~ k, Cod f ~ (->)) => Representable f repObj -> k repObj z -> f :% z
- covariantHomRepr :: Category k => Obj k x -> Representable (x :*-: k) x
- contravariantHomRepr :: Category k => Obj k x -> Representable (k :-*: x) x
- type InitialUniversal x u a = Representable (x :*%: 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 (u :%*: x) 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
- adjunctionInitialProp :: Adjunction c d f g -> Obj d y -> InitialUniversal y g (f :% y)
- adjunctionTerminalProp :: Adjunction c d f g -> Obj c x -> TerminalUniversal x f (g :% x)
- initialPropAdjunction :: forall f g c d. (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall y. InitialUniversal y g (f :% y)) -> Adjunction c d f g
- terminalPropAdjunction :: forall f g c d. (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall x. TerminalUniversal x f (g :% x)) -> Adjunction c d f g
Documentation
data Representable f repObj Source #
Constructors
| Representable | |
Fields
| |
unrepresent :: (Functor f, Dom f ~ k, Cod f ~ (->)) => Representable f repObj -> k repObj z -> f :% z Source #
covariantHomRepr :: Category k => Obj k x -> Representable (x :*-: k) x Source #
contravariantHomRepr :: Category k => Obj k x -> Representable (k :-*: x) x Source #
type InitialUniversal x u a = Representable (x :*%: u) a Source #
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 Source #
An initial universal property, a universal morphism from x to u.
type TerminalUniversal x u a = Representable (u :%*: x) a Source #
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 Source #
A terminal universal property, a universal morphism from u to x.
adjunctionInitialProp :: Adjunction c d f g -> Obj d y -> InitialUniversal y g (f :% y) Source #
For an adjunction F -| G, each pair (FY, unit_Y) is an initial morphism from Y to G.
adjunctionTerminalProp :: Adjunction c d f g -> Obj c x -> TerminalUniversal x f (g :% x) Source #
For an adjunction F -| G, each pair (GX, counit_X) is a terminal morphism from F to X.
initialPropAdjunction :: forall f g c d. (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall y. InitialUniversal y g (f :% y)) -> Adjunction c d f g Source #
terminalPropAdjunction :: forall f g c d. (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall x. TerminalUniversal x f (g :% x)) -> Adjunction c d f g Source #