data-category-0.9: Category theory

LicenseBSD-style (see the file LICENSE)
Maintainersjoerd@w3future.com
Stabilityexperimental
Portabilitynon-portable
Safe HaskellSafe
LanguageHaskell2010

Data.Category.Unit

Description

 

Documentation

data Unit a b where Source #

Constructors

Unit :: Unit () () 
Instances
Category k => HasColimits Unit k Source #

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) Source #

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

Category k => HasLimits Unit k Source #

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) Source #

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

Category Unit Source #

Unit is the category with one object.

Instance details

Defined in Data.Category.Unit

Methods

src :: Unit a b -> Obj Unit a Source #

tgt :: Unit a b -> Obj Unit b Source #

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

HasBinaryCoproducts Unit Source #

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 Source #

Methods

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

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

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

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

HasBinaryProducts Unit Source #

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 Source #

Methods

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

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

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

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

HasInitialObject Unit Source #

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 Source #

HasTerminalObject Unit Source #

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 Source #

CartesianClosed Unit Source # 
Instance details

Defined in Data.Category.CartesianClosed

Associated Types

type Exponential Unit y z :: Kind k Source #

Methods

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

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

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

HasColimits j k => HasLeftKan (Const j Unit ()) k Source #

The left Kan extension of f along a functor to the unit category is the colimit of f.

Instance details

Defined in Data.Category.KanExtension

Methods

lan :: Const j Unit () -> Obj (Nat (Dom (Const j Unit ())) k) f -> Nat (Dom (Const j Unit ())) k f (LanFam (Const j Unit ()) k f :.: Const j Unit ()) Source #

lanFactorizer :: Nat (Dom (Const j Unit ())) k f (h :.: Const j Unit ()) -> Nat (Cod (Const j Unit ())) k (LanFam (Const j Unit ()) k f) h Source #

HasLimits j k => HasRightKan (Const j Unit ()) k Source #

The right Kan extension of f along a functor to the unit category is the limit of f.

Instance details

Defined in Data.Category.KanExtension

Methods

ran :: Const j Unit () -> Obj (Nat (Dom (Const j Unit ())) k) f -> Nat (Dom (Const j Unit ())) k (RanFam (Const j Unit ()) k f :.: Const j Unit ()) f Source #

ranFactorizer :: Nat (Dom (Const j Unit ())) k (h :.: Const j Unit ()) f -> Nat (Cod (Const j Unit ())) k h (RanFam (Const j Unit ()) k f) Source #

type ColimitFam Unit k f Source # 
Instance details

Defined in Data.Category.Limit

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

Defined in Data.Category.Limit

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

Defined in Data.Category.Limit

type TerminalObject Unit Source # 
Instance details

Defined in Data.Category.Limit

type BinaryCoproduct Unit () () Source # 
Instance details

Defined in Data.Category.Limit

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

Defined in Data.Category.Limit

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

Defined in Data.Category.CartesianClosed

type Exponential Unit () () = ()
type LanFam (Const j Unit ()) k f Source # 
Instance details

Defined in Data.Category.KanExtension

type LanFam (Const j Unit ()) k f = Const Unit k (ColimitFam j k f)
type RanFam (Const j Unit ()) k f Source # 
Instance details

Defined in Data.Category.KanExtension

type RanFam (Const j Unit ()) k f = Const Unit k (LimitFam j k f)