data-category-0.8.1: Category theory
LicenseBSD-style (see the file LICENSE)
Maintainersjoerd@w3future.com
Stabilityexperimental
Portabilitynon-portable
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.Category.Unit

Description

 

Documentation

data Unit a b where #

Constructors

Unit :: Unit () () 

Instances

Instances details
Category k => HasColimits Unit k #

The colimit of a single object is that object.

Instance details

Defined in Data.Category.Limit

Methods

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

colimitFactorizer :: Cocone Unit k f n -> k (ColimitFam Unit k f) n #

Category k => HasLimits Unit k #

The limit of a single object is that object.

Instance details

Defined in Data.Category.Limit

Methods

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

limitFactorizer :: Cone Unit k f n -> k n (LimitFam Unit k f) #

Category Unit #

Unit is the category with one object.

Instance details

Defined in Data.Category.Unit

Methods

src :: forall (a :: k) (b :: k). Unit a b -> Obj Unit a #

tgt :: forall (a :: k) (b :: k). Unit a b -> Obj Unit b #

(.) :: forall (b :: k) (c :: k) (a :: k). Unit b c -> Unit a b -> Unit a c #

HasBinaryCoproducts Unit #

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

Instance details

Defined in Data.Category.Limit

Associated Types

type BinaryCoproduct Unit x y :: Kind k #

Methods

inj1 :: forall (x :: k) (y :: k). Obj Unit x -> Obj Unit y -> Unit x (BinaryCoproduct Unit x y) #

inj2 :: forall (x :: k) (y :: k). Obj Unit x -> Obj Unit y -> Unit y (BinaryCoproduct Unit x y) #

(|||) :: forall (x :: k) (a :: k) (y :: k). Unit x a -> Unit y a -> Unit (BinaryCoproduct Unit x y) a #

(+++) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). 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.

Instance details

Defined in Data.Category.Limit

Associated Types

type BinaryProduct Unit x y :: Kind k #

Methods

proj1 :: forall (x :: k) (y :: k). Obj Unit x -> Obj Unit y -> Unit (BinaryProduct Unit x y) x #

proj2 :: forall (x :: k) (y :: k). Obj Unit x -> Obj Unit y -> Unit (BinaryProduct Unit x y) y #

(&&&) :: forall (a :: k) (x :: k) (y :: k). Unit a x -> Unit a y -> Unit a (BinaryProduct Unit x y) #

(***) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). 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.

Instance details

Defined in Data.Category.Limit

Associated Types

type InitialObject Unit :: Kind k #

Methods

initialObject :: Obj Unit (InitialObject Unit) #

initialize :: forall (a :: k). Obj Unit a -> Unit (InitialObject Unit) a #

HasTerminalObject Unit #

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

Instance details

Defined in Data.Category.Limit

Associated Types

type TerminalObject Unit :: Kind k #

CartesianClosed Unit # 
Instance details

Defined in Data.Category.CartesianClosed

Associated Types

type Exponential Unit y z :: Kind k #

Methods

apply :: forall (y :: k) (z :: k). Obj Unit y -> Obj Unit z -> Unit (BinaryProduct Unit (Exponential Unit y z) y) z #

tuple :: forall (y :: k) (z :: k). Obj Unit y -> Obj Unit z -> Unit z (Exponential Unit y (BinaryProduct Unit z y)) #

(^^^) :: forall (z1 :: k) (z2 :: k) (y2 :: k) (y1 :: k). Unit z1 z2 -> Unit y2 y1 -> Unit (Exponential Unit y1 z1) (Exponential Unit y2 z2) #

type ColimitFam Unit k f # 
Instance details

Defined in Data.Category.Limit

type ColimitFam Unit k f = f :% ()
type LimitFam Unit k f # 
Instance details

Defined in Data.Category.Limit

type LimitFam Unit k f = f :% ()
type InitialObject Unit # 
Instance details

Defined in Data.Category.Limit

type TerminalObject Unit # 
Instance details

Defined in Data.Category.Limit

type BinaryCoproduct Unit () () # 
Instance details

Defined in Data.Category.Limit

type BinaryCoproduct Unit () () = ()
type BinaryProduct Unit () () # 
Instance details

Defined in Data.Category.Limit

type BinaryProduct Unit () () = ()
type Exponential Unit () () # 
Instance details

Defined in Data.Category.CartesianClosed

type Exponential Unit () () = ()