data-category-0.5.1.0: Category theory
data Void a b Source
Void is the category with no objects.
An initial object is the colimit of the functor from 0 to k.
A terminal object is the limit of the functor from 0 to k.
magic :: Void a b -> xSource
voidNat :: (Functor f, Functor g, Category d, Dom f ~ Void, Dom g ~ Void, Cod f ~ d, Cod g ~ d) => f -> g -> Nat Void d f gSource
data Magic k Source
Since there is nothing to map in Void, there's a functor from it to any other category.
Produced by Haddock version 2.13.2