Data.Category.Unit

Documentation

data Unit a b where

Constructors

Unit :: Unit () ()

Instances

Category Unit

Unit is the category with one object.

Defined in Data.Category.Unit

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.

Defined in Data.Category.Limit

Associated Types

type BinaryCoproduct Unit x y :: Type

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.

Defined in Data.Category.Limit

Associated Types

type BinaryProduct Unit x y :: Type

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.

Defined in Data.Category.Limit

Associated Types

type InitialObject Unit :: Type

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.

Defined in Data.Category.Limit

Associated Types

type TerminalObject Unit :: Type

Methods

terminalObject :: Obj Unit (TerminalObject Unit)

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

CartesianClosed Unit

Defined in Data.Category.CartesianClosed

Associated Types

type Exponential Unit y z :: Type

Methods

apply :: Obj Unit y -> Obj Unit z -> Unit (BinaryProduct Unit (Exponential Unit y z) y) z

tuple :: Obj Unit y -> Obj Unit z -> Unit z (Exponential Unit y (BinaryProduct Unit z y))

(^^^) :: Unit z1 z2 -> Unit y2 y1 -> Unit (Exponential Unit y1 z1) (Exponential Unit y2 z2)

Category k => HasColimits Unit k

The colimit of a single object is that object.

Defined in Data.Category.Limit

Methods

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

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

Category k => HasLimits Unit k

The limit of a single object is that object.

Defined in Data.Category.Limit

Methods

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

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

type InitialObject Unit

Defined in Data.Category.Limit

type InitialObject Unit = ()

type TerminalObject Unit

Defined in Data.Category.Limit

type TerminalObject Unit = ()

type BinaryCoproduct Unit () ()

Defined in Data.Category.Limit

type BinaryCoproduct Unit () () = ()

type BinaryProduct Unit () ()

Defined in Data.Category.Limit

type BinaryProduct Unit () () = ()

type ColimitFam Unit k f

Defined in Data.Category.Limit

type ColimitFam Unit k f = f :% ()

type LimitFam Unit k f

Defined in Data.Category.Limit

type LimitFam Unit k f = f :% ()

type Exponential Unit () ()

Defined in Data.Category.CartesianClosed

type Exponential Unit () () = ()