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

Data.Category.Cube

Description

The cube category.

Documentation

data Z #

Instances details

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

data S n #

Instances details

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

data Sign #

Constructors

M
P

data Cube :: * -> * -> * where #

Constructors

Instances details

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

Constructors

data ACube :: * -> * where #

Constructors

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

Constructors

Instances details

Functor Forget #	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 # type Cod Forget :: Type -> Type -> Type # type Forget :% a # Methods (%) :: Forget -> Dom Forget a b -> Cod Forget (Forget :% a) (Forget :% b) #
type Dom Forget #
Instance details Defined in Data.Category.Cube type Dom Forget = Cube
type Cod Forget #
Instance details Defined in Data.Category.Cube type Cod Forget = (->) :: Type -> Type -> Type
type Forget :% n #
Instance details Defined in Data.Category.Cube type Forget :% n = ACube n

data Add #

Constructors

Instances details

Functor Add #	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 # type Cod Add :: Type -> Type -> Type # type Add :% a # Methods (%) :: Add -> Dom Add a b -> Cod Add (Add :% a) (Add :% b) #
TensorProduct Add #
Instance details Defined in Data.Category.Cube Associated Types type Unit Add # Methods unitObject :: Add -> Obj (Cod Add) (Unit Add) # leftUnitor :: Cod Add ~ k => Add -> Obj k a -> k (Add :% (Unit Add, a)) a # leftUnitorInv :: Cod Add ~ k => Add -> Obj k a -> k a (Add :% (Unit Add, a)) # rightUnitor :: Cod Add ~ k => Add -> Obj k a -> k (Add :% (a, Unit Add)) a # rightUnitorInv :: Cod Add ~ k => Add -> Obj k a -> k a (Add :% (a, Unit Add)) # 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))) # 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)) #
type Dom Add #
Instance details Defined in Data.Category.Cube type Dom Add = Cube :**: Cube
type Cod Add #
Instance details Defined in Data.Category.Cube type Cod Add = Cube
type Unit Add #
Instance details Defined in Data.Category.Cube type Unit Add = Z
type Add :% (S m, n) #
Instance details Defined in Data.Category.Cube type Add :% (S m, n) = S (Add :% (m, n))
type Add :% (Z, n) #
Instance details Defined in Data.Category.Cube type Add :% (Z, n) = n