Data.Category.Cube

The cube category.

Documentation

data Z

Instances

type Add :% (Z, n)

type Add :% (Z, n) = n

data S n

Instances

type Add :% (S m, n)

type Add :% (S m, n) = S ((:%) Add (m, n))

data Sign

Constructors

M

P

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

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

Category Cube

Methods

src :: Cube a b -> Obj Cube a

tgt :: Cube a b -> Obj Cube b

(.) :: Cube b c -> Cube a b -> Cube a c

HasTerminalObject Cube

Associated Types

type TerminalObject (Cube :: * -> * -> *) :: *

Methods

terminalObject :: Obj Cube (TerminalObject Cube)

terminate :: Obj Cube a -> Cube a (TerminalObject Cube)

type TerminalObject Cube

type TerminalObject Cube = Z

data Sign0

Constructors

SM

S0

SP

data ACube :: * -> * where

Constructors

Nil :: ACube Z

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

data Forget

Constructors

Forget

Instances

Functor Forget

Turn Cube x y arrows into ACube x -> ACube y functions.

Associated Types

type Dom Forget :: * -> * -> *

type Cod Forget :: * -> * -> *

type Forget :% a :: *

Methods

(%) :: Forget -> Dom Forget a b -> Cod Forget (Forget :% a) (Forget :% b)

type Dom Forget

type Dom Forget = Cube

type Cod Forget

type Cod Forget = (->)

type Forget :% n

type Forget :% n = ACube n

data Add

Constructors

Add

Instances

Functor Add

Ordinal addition is a bifuntor, it concattenates the maps as it were.

Associated Types

type Dom Add :: * -> * -> *

type Cod Add :: * -> * -> *

type Add :% a :: *

Methods

(%) :: Add -> Dom Add a b -> Cod Add (Add :% a) (Add :% b)

TensorProduct Add

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

type Dom Add = (:**:) Cube Cube

type Cod Add

type Cod Add = Cube

type Unit Add

type Unit Add = Z

type Add :% (S m, n)

type Add :% (S m, n) = S ((:%) Add (m, n))

type Add :% (Z, n)

type Add :% (Z, n) = n