Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- class Symmetric cat t => Semicartesian cat t where
- (/\) :: Semicartesian cat t => cat a x -> cat a y -> cat a (x `t` y)
- class Symmetric cat t => Semicocartesian cat t where
- (\/) :: Semicocartesian cat t => cat x a -> cat y a -> cat (x `t` y) a
- class (Semicartesian cat t, Tensor cat t i) => Cartesian cat t i | i -> t, t -> i where
- class (Semicocartesian cat t, Tensor cat t i) => Cocartesian cat t i | i -> t, t -> i where
Semicartesian
class Symmetric cat t => Semicartesian cat t where Source #
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
split :: cat a (a `t` a) Source #
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) Source #
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 Source # | |
Semicartesian (->) (,) Source # | |
(/\) :: Semicartesian cat t => cat a x -> cat a y -> cat a (x `t` y) infixr 9 Source #
Infix version of fork
.
Semicocartesian
class Symmetric cat t => Semicocartesian cat t where Source #
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
merge :: cat (a `t` a) a Source #
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 Source #
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 Source # | |
Semicocartesian (->) Either Source # | |
(\/) :: Semicocartesian cat t => cat x a -> cat y a -> cat (x `t` y) a infixr 9 Source #
Infix version of fuse
.
Cartesian
class (Semicartesian cat t, Tensor cat t i) => Cartesian cat t i | i -> t, t -> i where Source #
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
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 Source #
The left projection for t
.
Examples
>>>
projl @(->) @(,) (True, "hello")
True
projr :: cat (x `t` y) y Source #
The right projection for t
.
Examples
>>>
projr @(->) @(,) (True, "hello")
"hello"
unfork :: cat a (x `t` y) -> (cat a x, cat a y) Source #
Given the universal map cat a (x
, construct morphisms t
y)cat a x
and cat a y
.
Examples
Cocartesian
class (Semicocartesian cat t, Tensor cat t i) => Cocartesian cat t i | i -> t, t -> i where Source #
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
A morphism from the initial object i
in cat
to a
.
Examples
incll :: cat x (x `t` y) Source #
The left inclusion for t
.
Examples
inclr :: cat y (x `t` y) Source #
The right inclusion for t
.
Examples
unfuse :: cat (x `t` y) a -> (cat x a, cat y a) Source #
Given the universal map cat (x
, construct morphisms t
y) acat x a
and cat y a
.
Examples
Instances
Cartesian (->) t i => Cocartesian Op t i Source # | |
Cocartesian (->) Either Void Source # | |