Data.Category.Cube

The cube category.

Documentation

data Z

Instances

type Add :% (Z, n)

Defined in Data.Category.Cube

type Add :% (Z, n) = n

data S n

Instances

type Add :% (S m, n)

Defined in Data.Category.Cube

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

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

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

Defined in Data.Category.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.

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

Defined in Data.Category.Cube

type Dom Forget = Cube

type Cod Forget

Defined in Data.Category.Cube

type Cod Forget = (->) :: Type -> Type -> Type

type Forget :% n

Defined in Data.Category.Cube

type Forget :% n = ACube n

data Add

Constructors

Add

Instances

Functor Add

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

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

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

Defined in Data.Category.Cube

type Dom Add = Cube :**: Cube

type Cod Add

Defined in Data.Category.Cube

type Cod Add = Cube

type Unit Add

Defined in Data.Category.Cube

type Unit Add = Z

type Add :% (S m, n)

Defined in Data.Category.Cube

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

type Add :% (Z, n)

Defined in Data.Category.Cube

type Add :% (Z, n) = n