License	BSD-style (see the file LICENSE)
Maintainer	sjoerd@w3future.com
Stability	experimental
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Category.Cube

Description

The cube category.

Documentation

data Z Source #

Instances

Instances details

type Add :% (Z, n) Source #
Instance details Defined in Data.Category.Cube type Add :% (Z, n) = n

data S n Source #

Instances

Instances details

type Add :% (S m, n) Source #
Instance details Defined in Data.Category.Cube type Add :% (S m, n) = S (Add :% (m, n))

data Sign Source #

Constructors

M
P

data Cube :: Type -> Type -> Type where Source #

Constructors

Z :: Cube Z Z
S :: Cube x y -> Cube (S x) (S y)
Y :: Sign -> Cube x y -> Cube x (S y)
X :: Cube x y -> Cube (S x) y

Instances

Instances details

Category Cube Source #
Instance details Defined in Data.Category.Cube Methods src :: forall (a :: k) (b :: k). Cube a b -> Obj Cube a Source # tgt :: forall (a :: k) (b :: k). Cube a b -> Obj Cube b Source # (.) :: forall (b :: k) (c :: k) (a :: k). Cube b c -> Cube a b -> Cube a c Source #
HasTerminalObject Cube Source #
Instance details Defined in Data.Category.Cube Associated Types type TerminalObject Cube :: Kind k Source # Methods terminalObject :: Obj Cube (TerminalObject Cube) Source # terminate :: forall (a :: k). Obj Cube a -> Cube a (TerminalObject Cube) Source #
type TerminalObject Cube Source #
Instance details Defined in Data.Category.Cube type TerminalObject Cube = Z

data Sign0 Source #

Constructors

SM
S0
SP

data ACube :: Type -> Type where Source #

Constructors

Nil :: ACube Z
Cons :: Sign0 -> ACube n -> ACube (S n)

data Forget Source #

Constructors

Forget

Instances

Instances details

Functor Forget Source #	Turn `Cube x y` arrows into `ACube x -> ACube y` functions.
Instance details Defined in Data.Category.Cube Associated Types type Dom Forget :: Type -> Type -> Type Source # type Cod Forget :: Type -> Type -> Type Source # type Forget :% a Source # Methods (%) :: Forget -> Dom Forget a b -> Cod Forget (Forget :% a) (Forget :% b) Source #
type Cod Forget Source #
Instance details Defined in Data.Category.Cube type Cod Forget = (->)
type Dom Forget Source #
Instance details Defined in Data.Category.Cube type Dom Forget = Cube
type Forget :% n Source #
Instance details Defined in Data.Category.Cube type Forget :% n = ACube n

data Add Source #

Constructors

Add

Instances

Instances details

Functor Add Source #	Ordinal addition is a bifuntor, it concattenates the maps as it were.
Instance details Defined in Data.Category.Cube Associated Types type Dom Add :: Type -> Type -> Type Source # type Cod Add :: Type -> Type -> Type Source # type Add :% a Source # Methods (%) :: Add -> Dom Add a b -> Cod Add (Add :% a) (Add :% b) Source #
TensorProduct Add Source #
Instance details Defined in Data.Category.Cube Associated Types type Unit Add :: Kind (Cod f) Source # Methods unitObject :: Add -> Obj (Cod Add) (Unit Add) Source # leftUnitor :: Cod Add ~ k => Add -> Obj k a -> k (Add :% (Unit Add, a)) a Source # leftUnitorInv :: Cod Add ~ k => Add -> Obj k a -> k a (Add :% (Unit Add, a)) Source # rightUnitor :: Cod Add ~ k => Add -> Obj k a -> k (Add :% (a, Unit Add)) a Source # rightUnitorInv :: Cod Add ~ k => Add -> Obj k a -> k a (Add :% (a, Unit Add)) Source # associator :: Cod Add ~ k => Add -> Obj k a -> Obj k b -> Obj k c -> k (Add :% (Add :% (a, b), c)) (Add :% (a, Add :% (b, c))) Source # associatorInv :: Cod Add ~ k => Add -> Obj k a -> Obj k b -> Obj k c -> k (Add :% (a, Add :% (b, c))) (Add :% (Add :% (a, b), c)) Source #
type Cod Add Source #
Instance details Defined in Data.Category.Cube type Cod Add = Cube
type Dom Add Source #
Instance details Defined in Data.Category.Cube type Dom Add = Cube :**: Cube
type Unit Add Source #
Instance details Defined in Data.Category.Cube type Unit Add = Z
type Add :% (S m, n) Source #
Instance details Defined in Data.Category.Cube type Add :% (S m, n) = S (Add :% (m, n))
type Add :% (Z, n) Source #
Instance details Defined in Data.Category.Cube type Add :% (Z, n) = n