Data.Category.Unit

Documentation

data Unit a b where

Constructors

Unit :: Unit () ()

Instances

Category Unit

Unit is the category with one object.

Methods

src :: Unit a b -> Obj Unit a

tgt :: Unit a b -> Obj Unit b

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

HasBinaryCoproducts Unit

In the category of one object that object is its own coproduct.

Associated Types

type BinaryCoproduct (Unit :: * -> * -> *) x y :: *

Methods

inj1 :: Obj Unit x -> Obj Unit y -> Unit x (BinaryCoproduct Unit x y)

inj2 :: Obj Unit x -> Obj Unit y -> Unit y (BinaryCoproduct Unit x y)

(|||) :: Unit x a -> Unit y a -> Unit (BinaryCoproduct Unit x y) a

(+++) :: Unit a1 b1 -> Unit a2 b2 -> Unit (BinaryCoproduct Unit a1 a2) (BinaryCoproduct Unit b1 b2)

HasBinaryProducts Unit

In the category of one object that object is its own product.

Associated Types

type BinaryProduct (Unit :: * -> * -> *) x y :: *

Methods

proj1 :: Obj Unit x -> Obj Unit y -> Unit (BinaryProduct Unit x y) x

proj2 :: Obj Unit x -> Obj Unit y -> Unit (BinaryProduct Unit x y) y

(&&&) :: Unit a x -> Unit a y -> Unit a (BinaryProduct Unit x y)

(***) :: Unit a1 b1 -> Unit a2 b2 -> Unit (BinaryProduct Unit a1 a2) (BinaryProduct Unit b1 b2)

HasInitialObject Unit

The category of one object has that object as initial object.

Associated Types

type InitialObject (Unit :: * -> * -> *) :: *

Methods

initialObject :: Obj Unit (InitialObject Unit)

initialize :: Obj Unit a -> Unit (InitialObject Unit) a

HasTerminalObject Unit

The category of one object has that object as terminal object.

Associated Types

type TerminalObject (Unit :: * -> * -> *) :: *

Methods

terminalObject :: Obj Unit (TerminalObject Unit)

terminate :: Obj Unit a -> Unit a (TerminalObject Unit)

Category k => HasColimits Unit k

The colimit of a single object is that object.

Methods

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

colimitFactorizer :: Obj (Nat Unit k) f -> forall n. Cocone f n -> k (Colimit f) n

Category k => HasLimits Unit k

The limit of a single object is that object.

Methods

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

limitFactorizer :: Obj (Nat Unit k) f -> forall n. Cone f n -> k n (Limit f)

type InitialObject Unit

type InitialObject Unit = ()

type TerminalObject Unit

type TerminalObject Unit = ()

type BinaryCoproduct Unit () ()

type BinaryCoproduct Unit () () = ()

type BinaryProduct Unit () ()

type BinaryProduct Unit () () = ()

type ColimitFam Unit k f

type ColimitFam Unit k f = (:%) f ()

type LimitFam Unit k f

type LimitFam Unit k f = (:%) f ()