Control.Morphism.Universal

Note the choice of which is universal and which is couniversal is chosen to make the definitions consistent with limits and colimits.

Documentation

data Couniversal a f x

Constructors

Couniversal (a -> f x) (forall z. (a -> f z) -> x -> z)

extractCouniversal :: Couniversal a f x -> a -> f x

couniversalize :: (a -> f z) -> Couniversal a f x -> x -> z

couniversalIdentity :: Couniversal a Identity a

data Universal a f x

Constructors

Universal (f x -> a) (forall z. (f z -> a) -> z -> x)

extractUniversal :: Universal a f x -> f x -> a

universalize :: Universal a f x -> (f z -> a) -> z -> x

universalIdentity :: Universal a Identity a