Control.Category.Cartesian

Semicartesian

class Symmetric cat t => Semicartesian cat t where

A Category is Semicartesian if it is equipped with a Symmetric bifunctor t and each object comes equipped with a diagonal morphism \(\Delta_x: x \to x \otimes x \), which we call split.

Laws

grmap split . split ≡ bwd assoc . glmap split . split
glmap split . split ≡ fwd assoc . grmap split . split

Minimal complete definition

split

Methods

split :: cat a (a `t` a)

The diagonal morphism of a in cat. We can think of split as duplicating data.

Examples

>>> split @(->) @(,) True
(True,True)

fork :: cat a x -> cat a y -> cat a (x `t` y)

Given morphisms cat a x and cat a y, construct the universal map cat a (x `t` y).

Examples

>>> :t fork @(->) @(,) show not
fork @(->) @(,) show not :: Bool -> (String, Bool)

>>> fork @(->) @(,) show not True
("True",False)

Instances

Semicocartesian (->) t => Semicartesian Op t

Defined in Control.Category.Cartesian

Methods

split :: Op a (t a a)

fork :: Op a x -> Op a y -> Op a (t x y)

Semicartesian (->) (,)

Defined in Control.Category.Cartesian

Methods

split :: a -> (a, a)

fork :: (a -> x) -> (a -> y) -> a -> (x, y)

(/\) :: Semicartesian cat t => cat a x -> cat a y -> cat a (x `t` y) infixr 9

Infix version of fork.

Semicocartesian

class Symmetric cat t => Semicocartesian cat t where

A Category is Semicocartesian if it is equipped with a Symmetric type operator t and each object comes equipped with a morphism \(\Delta^{-1}_x: x \otimes x \to x\), which we call merge.

Laws

merge . grmap merge ≡ merge . glmap merge . fwd assoc
merge . glmap merge ≡ merge . grmap merge . bwd assoc

Minimal complete definition

merge

Methods

merge :: cat (a `t` a) a

The co-diagonal morphism of a in cat.

Examples

>>> :t merge @(->) @(Either) (Left True)
merge @(->) @(Either) (Left True) :: Bool

>>> merge @(->) @(Either) (Left True)
True

fuse :: cat x a -> cat y a -> cat (x `t` y) a

Given morphisms cat x a and cat y a, construct the universal map cat (x `t` y) a.

Examples

Instances

Semicartesian (->) t => Semicocartesian Op t

Defined in Control.Category.Cartesian

Methods

merge :: Op (t a a) a

fuse :: Op x a -> Op y a -> Op (t x y) a

Semicocartesian (->) Either

Defined in Control.Category.Cartesian

Methods

merge :: Either a a -> a

fuse :: (x -> a) -> (y -> a) -> Either x y -> a

(\/) :: Semicocartesian cat t => cat x a -> cat y a -> cat (x `t` y) a infixr 9

Infix version of fuse.

Cartesian

class (Semicartesian cat t, Tensor cat t i) => Cartesian cat t i | i -> t, t -> i where

A Category equipped with a Tensor t where the Tensor unit i is the terminal object in cat and thus every object a is equipped with a morphism \(e_x: x \to I\), which we call kill.

Laws

fwd unitl . glmap kill . split ≡ id
fwd unitr . grmap kill . split ≡ id

Minimal complete definition

kill

Methods

kill :: cat a i

A morphism from the a to the terminal object i in @cat. We can think of kill as deleting data where split duplicates it.

Examples

>>> kill @(->) @(,) @() True
()

projl :: cat (x `t` y) x

The left projection for t.

Examples

>>> projl @(->) @(,) (True, "hello")
True

projr :: cat (x `t` y) y

The right projection for t.

Examples

>>> projr @(->) @(,) (True, "hello")
"hello"

unfork :: cat a (x `t` y) -> (cat a x, cat a y)

Given the universal map cat a (x t y), construct morphisms cat a x and cat a y.

Examples

Instances

Cocartesian (->) t i => Cartesian Op t i

Defined in Control.Category.Cartesian

Methods

kill :: Op a i

projl :: Op (t x y) x

projr :: Op (t x y) y

unfork :: Op a (t x y) -> (Op a x, Op a y)

Cartesian (->) (,) ()

Defined in Control.Category.Cartesian

Methods

kill :: a -> ()

projl :: (x, y) -> x

projr :: (x, y) -> y

unfork :: (a -> (x, y)) -> (a -> x, a -> y)

Cocartesian

class (Semicocartesian cat t, Tensor cat t i) => Cocartesian cat t i | i -> t, t -> i where

A Category equipped with a Tensor t where the Tensor unit i is the initial object in cat and thus every object a is equipped with a morphism \(e^{-1}_x: I \to x\), which we call spawn.

Laws

merge . glmap spawn . bwd unitl ≡ id
merge . grmap spawn . bwd unitr ≡ id

Minimal complete definition

spawn

Methods

spawn :: cat i a

A morphism from the initial object i in cat to a.

Examples

incll :: cat x (x `t` y)

The left inclusion for t.

Examples

inclr :: cat y (x `t` y)

The right inclusion for t.

Examples

unfuse :: cat (x `t` y) a -> (cat x a, cat y a)

Given the universal map cat (x t y) a, construct morphisms cat x a and cat y a.

Examples

Instances

Cartesian (->) t i => Cocartesian Op t i

Defined in Control.Category.Cartesian

Methods

spawn :: Op i a

incll :: Op x (t x y)

inclr :: Op y (t x y)

unfuse :: Op (t x y) a -> (Op x a, Op y a)

Cocartesian (->) Either Void

Defined in Control.Category.Cartesian

Methods

spawn :: Void -> a

incll :: x -> Either x y

inclr :: y -> Either x y

unfuse :: (Either x y -> a) -> (x -> a, y -> a)