Data.Category.Void

0, the empty category. The limit and colimit of the functor from 0 to some category provide terminal and initial objects in that category.

Documentation

data Void a b

The (empty) data type of the arrows in 0.

Instances

Category Void

HasInitialObject ~> => HasColimits Void ~>

HasTerminalObject ~> => HasLimits Void ~>

magicVoid :: Void a b -> x

magicVoidO :: Obj Void a -> x

data VoidDiagram (~>)

The functor from 0 to (~>), the empty diagram in (~>).

Constructors

VoidDiagram

Instances

Functor (VoidDiagram ~>)

voidNat :: (Functor f, Functor g, Dom f ~ Void, Dom g ~ Void, Cod f ~ d, Cod g ~ d) => f -> g -> Nat Void d f g