data-category-0.11: Category theory
LicenseBSD-style (see the file LICENSE)
Maintainersjoerd@w3future.com
Stabilityexperimental
Portabilitynon-portable
Safe HaskellSafe-Inferred
LanguageHaskell2010

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 #

type TerminalObject Cube Source # 
Instance details

Defined in Data.Category.Cube

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