data-category-0.7.2: Category theory

LicenseBSD-style (see the file LICENSE)
Maintainersjoerd@w3future.com
Stabilityexperimental
Portabilitynon-portable
Safe HaskellSafe
LanguageHaskell2010

Data.Category.RepresentableFunctor

Description

 
Synopsis

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 #

type InitialUniversal x u a = Representable ((x :*-: Cod u) :.: 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.

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.