Data.Category.Void

Documentation

data Void a b

Instances

Category Void

Void is the category with no objects.

(Category Void, Category k, HasInitialObject k) => HasColimits Void k

An initial object is the colimit of the functor from 0 to k.

(Category Void, Category k, HasTerminalObject k) => HasLimits Void k

A terminal object is the limit of the functor from 0 to k.

magic :: Void a b -> x

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 g

data Magic k

Constructors

Magic

Instances

(Category (Dom (Magic k)), Category (Cod (Magic k)), Category k) => Functor (Magic k)

Since there is nothing to map in Void, there's a functor from it to any other category.