Data.Category.Void

Documentation

data Void a b

Instances

Category Void

Void is the category with no objects.

Defined in Data.Category.Void

Methods

src :: Void a b -> Obj Void a

tgt :: Void a b -> Obj Void b

(.) :: Void b c -> Void a b -> Void a c

HasInitialObject k => HasColimits Void k

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

Defined in Data.Category.Limit

Methods

colimit :: Obj (Nat Void k) f -> Cocone f (Colimit f)

colimitFactorizer :: Obj (Nat Void k) f -> Cocone f n -> k (Colimit f) n

HasTerminalObject k => HasLimits Void k

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

Defined in Data.Category.Limit

Methods

limit :: Obj (Nat Void k) f -> Cone f (Limit f)

limitFactorizer :: Obj (Nat Void k) f -> Cone f n -> k n (Limit f)

type ColimitFam Void k f

Defined in Data.Category.Limit

type ColimitFam Void k f = InitialObject k

type LimitFam Void k f

Defined in Data.Category.Limit

type LimitFam Void k f = TerminalObject k

magic :: Void a b -> x

voidNat :: (Functor f, Functor g, 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 k => Functor (Magic k)

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

Defined in Data.Category.Void

Associated Types

type Dom (Magic k) :: Type -> Type -> Type

type Cod (Magic k) :: Type -> Type -> Type

type (Magic k) :% a :: Type

Methods

(%) :: Magic k -> Dom (Magic k) a b -> Cod (Magic k) (Magic k :% a) (Magic k :% b)

type Dom (Magic k)

Defined in Data.Category.Void

type Dom (Magic k) = Void

type Cod (Magic k)

Defined in Data.Category.Void

type Cod (Magic k) = k