{-# LANGUAGE TypeFamilies, GADTs, RankNTypes, TypeOperators, UndecidableInstances, NoImplicitPrelude #-}
module Data.Category.Cube where
import Data.Category
import Data.Category.Product
import Data.Category.Functor
import Data.Category.Monoidal
import Data.Category.Limit
data Z
data S n
data Sign = M | P
data Cube :: * -> * -> * where
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
instance Category Cube where
src :: Cube a b -> Obj Cube a
src Cube a b
Z = Obj Cube a
Cube Z Z
Z
src (S Cube x y
c) = Cube x x -> Cube (S x) (S x)
forall x y. Cube x y -> Cube (S x) (S y)
S (Cube x y -> Cube x x
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Cube x y
c)
src (Y Sign
_ Cube a y
c) = Cube a y -> Obj Cube a
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Cube a y
c
src (X Cube x b
c) = Cube x x -> Cube (S x) (S x)
forall x y. Cube x y -> Cube (S x) (S y)
S (Cube x b -> Cube x x
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Cube x b
c)
tgt :: Cube a b -> Obj Cube b
tgt Cube a b
Z = Obj Cube b
Cube Z Z
Z
tgt (S Cube x y
c) = Cube y y -> Cube (S y) (S y)
forall x y. Cube x y -> Cube (S x) (S y)
S (Cube x y -> Cube y y
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Cube x y
c)
tgt (Y Sign
_ Cube a y
c) = Cube y y -> Cube (S y) (S y)
forall x y. Cube x y -> Cube (S x) (S y)
S (Cube a y -> Cube y y
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Cube a y
c)
tgt (X Cube x b
c) = Cube x b -> Obj Cube b
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Cube x b
c
Cube b c
Z . :: Cube b c -> Cube a b -> Cube a c
. Cube a b
c = Cube a b
Cube a c
c
Cube b c
c . Cube a b
Z = Cube b c
Cube a c
c
S Cube x y
c . S Cube x y
d = Cube x y -> Cube (S x) (S y)
forall x y. Cube x y -> Cube (S x) (S y)
S (Cube x y
c Cube x y -> Cube x x -> Cube x y
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Cube x x
Cube x y
d)
S Cube x y
c . Y Sign
s Cube a y
d = Sign -> Cube a y -> Cube a (S y)
forall x y. Sign -> Cube x y -> Cube x (S y)
Y Sign
s (Cube x y
c Cube x y -> Cube a x -> Cube a y
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Cube a x
Cube a y
d)
Y Sign
s Cube b y
c . Cube a b
d = Sign -> Cube a y -> Cube a (S y)
forall x y. Sign -> Cube x y -> Cube x (S y)
Y Sign
s (Cube b y
c Cube b y -> Cube a b -> Cube a y
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Cube a b
d)
X Cube x c
c . S Cube x y
d = Cube x c -> Cube (S x) c
forall x y. Cube x y -> Cube (S x) y
X (Cube x c
c Cube x c -> Cube x x -> Cube x c
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Cube x x
Cube x y
d)
X Cube x c
c . Y Sign
_ Cube a y
d = Cube x c
c Cube x c -> Cube a x -> Cube a c
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Cube a x
Cube a y
d
Cube b c
c . X Cube x b
d = Cube x c -> Cube (S x) c
forall x y. Cube x y -> Cube (S x) y
X (Cube b c
c Cube b c -> Cube x b -> Cube x c
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Cube x b
d)
instance HasTerminalObject Cube where
type TerminalObject Cube = Z
terminalObject :: Obj Cube (TerminalObject Cube)
terminalObject = Obj Cube (TerminalObject Cube)
Cube Z Z
Z
terminate :: Obj Cube a -> Cube a (TerminalObject Cube)
terminate Obj Cube a
Z = Cube a (TerminalObject Cube)
Cube Z Z
Z
terminate (S Cube x y
f) = Cube x Z -> Cube (S x) Z
forall x y. Cube x y -> Cube (S x) y
X (Obj Cube x -> Cube x (TerminalObject Cube)
forall k (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate Obj Cube x
Cube x y
f)
data Sign0 = SM | S0 | SP
data ACube :: * -> * where
Nil :: ACube Z
Cons :: Sign0 -> ACube n -> ACube (S n)
data Forget = Forget
instance Functor Forget where
type Dom Forget = Cube
type Cod Forget = (->)
type Forget :% n = ACube n
Forget
Forget % :: Forget -> Dom Forget a b -> Cod Forget (Forget :% a) (Forget :% b)
% Dom Forget a b
Z = \ACube Z
x -> ACube Z
x
Forget
Forget % S f = \(Cons Sign0
s ACube n
x) -> Sign0 -> ACube y -> ACube (S y)
forall n. Sign0 -> ACube n -> ACube (S n)
Cons Sign0
s ((Forget
Forget Forget -> Dom Forget x y -> Cod Forget (Forget :% x) (Forget :% y)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom Forget x y
Cube x y
f) ACube n
x)
Forget
Forget % Y M f = \ACube a
x -> Sign0 -> ACube y -> ACube (S y)
forall n. Sign0 -> ACube n -> ACube (S n)
Cons Sign0
SM ((Forget
Forget Forget -> Dom Forget a y -> Cod Forget (Forget :% a) (Forget :% y)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom Forget a y
Cube a y
f) ACube a
x)
Forget
Forget % Y P f = \ACube a
x -> Sign0 -> ACube y -> ACube (S y)
forall n. Sign0 -> ACube n -> ACube (S n)
Cons Sign0
SP ((Forget
Forget Forget -> Dom Forget a y -> Cod Forget (Forget :% a) (Forget :% y)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom Forget a y
Cube a y
f) ACube a
x)
Forget
Forget % X f = \(Cons Sign0
_ ACube n
x) -> (Forget
Forget Forget -> Dom Forget x b -> Cod Forget (Forget :% x) (Forget :% b)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom Forget x b
Cube x b
f) ACube n
x
data Add = Add
instance Functor Add where
type Dom Add = Cube :**: Cube
type Cod Add = Cube
type Add :% (Z , n) = n
type Add :% (S m, n) = S (Add :% (m, n))
Add
Add % :: Add -> Dom Add a b -> Cod Add (Add :% a) (Add :% b)
% (Z :**: g) = Cod Add (Add :% a) (Add :% b)
Cube a2 b2
g
Add
Add % (S f :**: g) = Cube (Add :% (x, a2)) (Add :% (y, b2))
-> Cube (S (Add :% (x, a2))) (S (Add :% (y, b2)))
forall x y. Cube x y -> Cube (S x) (S y)
S (Add
Add Add
-> Dom Add (x, a2) (y, b2)
-> Cod Add (Add :% (x, a2)) (Add :% (y, b2))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (Cube x y
f Cube x y -> Cube a2 b2 -> (:**:) Cube Cube (x, a2) (y, b2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Cube a2 b2
g))
Add
Add % (Y s f :**: g) = Sign
-> Cube (Add :% (a1, a2)) (Add :% (y, b2))
-> Cube (Add :% (a1, a2)) (S (Add :% (y, b2)))
forall x y. Sign -> Cube x y -> Cube x (S y)
Y Sign
s (Add
Add Add
-> Dom Add (a1, a2) (y, b2)
-> Cod Add (Add :% (a1, a2)) (Add :% (y, b2))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (Cube a1 y
f Cube a1 y -> Cube a2 b2 -> (:**:) Cube Cube (a1, a2) (y, b2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Cube a2 b2
g))
Add
Add % (X f :**: g) = Cube (Add :% (x, a2)) (Add :% (b1, b2))
-> Cube (S (Add :% (x, a2))) (Add :% (b1, b2))
forall x y. Cube x y -> Cube (S x) y
X (Add
Add Add
-> Dom Add (x, a2) (b1, b2)
-> Cod Add (Add :% (x, a2)) (Add :% (b1, b2))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (Cube x b1
f Cube x b1 -> Cube a2 b2 -> (:**:) Cube Cube (x, a2) (b1, b2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Cube a2 b2
g))
instance TensorProduct Add where
type Unit Add = Z
unitObject :: Add -> Obj (Cod Add) (Unit Add)
unitObject Add
Add = Obj (Cod Add) (Unit Add)
Cube Z Z
Z
leftUnitor :: Add -> Obj k a -> k (Add :% (Unit Add, a)) a
leftUnitor Add
Add Obj k a
a = Obj k a
k (Add :% (Unit Add, a)) a
a
leftUnitorInv :: Add -> Obj k a -> k a (Add :% (Unit Add, a))
leftUnitorInv Add
Add Obj k a
a = Obj k a
k a (Add :% (Unit Add, a))
a
rightUnitor :: Add -> Obj k a -> k (Add :% (a, Unit Add)) a
rightUnitor Add
Add Obj k a
Z = k (Add :% (a, Unit Add)) a
Cube Z Z
Z
rightUnitor Add
Add (S n) = Cube (Add :% (y, Z)) x -> Cube (S (Add :% (y, Z))) (S x)
forall x y. Cube x y -> Cube (S x) (S y)
S (Add -> Obj Cube x -> Cube (Add :% (x, Unit Add)) x
forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k (f :% (a, Unit f)) a
rightUnitor Add
Add Obj Cube x
Cube x y
n)
rightUnitorInv :: Add -> Obj k a -> k a (Add :% (a, Unit Add))
rightUnitorInv Add
Add Obj k a
Z = k a (Add :% (a, Unit Add))
Cube Z Z
Z
rightUnitorInv Add
Add (S n) = Cube x (Add :% (y, Z)) -> Cube (S x) (S (Add :% (y, Z)))
forall x y. Cube x y -> Cube (S x) (S y)
S (Add -> Obj Cube x -> Cube x (Add :% (x, Unit Add))
forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k a (f :% (a, Unit f))
rightUnitorInv Add
Add Obj Cube x
Cube x y
n)
associator :: Add
-> Obj k a
-> Obj k b
-> Obj k c
-> k (Add :% (Add :% (a, b), c)) (Add :% (a, Add :% (b, c)))
associator Add
Add Obj k a
Z Obj k b
Z Obj k c
n = Obj k c
k (Add :% (Add :% (a, b), c)) (Add :% (a, Add :% (b, c)))
n
associator Add
Add Obj k a
Z (S m) Obj k c
n = Cube (Add :% (y, c)) (Add :% (y, c))
-> Cube (S (Add :% (y, c))) (S (Add :% (y, c)))
forall x y. Cube x y -> Cube (S x) (S y)
S (Add
-> Cube Z Z
-> Obj Cube x
-> Obj Cube c
-> Cube (Add :% (Add :% (Z, x), c)) (Add :% (Z, Add :% (x, c)))
forall f (k :: * -> * -> *) a b c.
(TensorProduct f, Cod f ~ k) =>
f
-> Obj k a
-> Obj k b
-> Obj k c
-> k (f :% (f :% (a, b), c)) (f :% (a, f :% (b, c)))
associator Add
Add Cube Z Z
Z Obj Cube x
Cube x y
m Obj k c
Obj Cube c
n)
associator Add
Add (S l) Obj k b
m Obj k c
n = Cube (Add :% (Add :% (y, b), c)) (Add :% (y, Add :% (b, c)))
-> Cube
(S (Add :% (Add :% (y, b), c))) (S (Add :% (y, Add :% (b, c))))
forall x y. Cube x y -> Cube (S x) (S y)
S (Add
-> Obj Cube x
-> Obj Cube b
-> Obj Cube c
-> Cube (Add :% (Add :% (x, b), c)) (Add :% (x, Add :% (b, c)))
forall f (k :: * -> * -> *) a b c.
(TensorProduct f, Cod f ~ k) =>
f
-> Obj k a
-> Obj k b
-> Obj k c
-> k (f :% (f :% (a, b), c)) (f :% (a, f :% (b, c)))
associator Add
Add Obj Cube x
Cube x y
l Obj k b
Obj Cube b
m Obj k c
Obj Cube c
n)
associatorInv :: Add
-> Obj k a
-> Obj k b
-> Obj k c
-> k (Add :% (a, Add :% (b, c))) (Add :% (Add :% (a, b), c))
associatorInv Add
Add Obj k a
Z Obj k b
Z Obj k c
n = Obj k c
k (Add :% (a, Add :% (b, c))) (Add :% (Add :% (a, b), c))
n
associatorInv Add
Add Obj k a
Z (S m) Obj k c
n = Cube (Add :% (y, c)) (Add :% (y, c))
-> Cube (S (Add :% (y, c))) (S (Add :% (y, c)))
forall x y. Cube x y -> Cube (S x) (S y)
S (Add
-> Cube Z Z
-> Obj Cube x
-> Obj Cube c
-> Cube (Add :% (Z, Add :% (x, c))) (Add :% (Add :% (Z, x), c))
forall f (k :: * -> * -> *) a b c.
(TensorProduct f, Cod f ~ k) =>
f
-> Obj k a
-> Obj k b
-> Obj k c
-> k (f :% (a, f :% (b, c))) (f :% (f :% (a, b), c))
associatorInv Add
Add Cube Z Z
Z Obj Cube x
Cube x y
m Obj k c
Obj Cube c
n)
associatorInv Add
Add (S l) Obj k b
m Obj k c
n = Cube (Add :% (y, Add :% (b, c))) (Add :% (Add :% (y, b), c))
-> Cube
(S (Add :% (y, Add :% (b, c)))) (S (Add :% (Add :% (y, b), c)))
forall x y. Cube x y -> Cube (S x) (S y)
S (Add
-> Obj Cube x
-> Obj Cube b
-> Obj Cube c
-> Cube (Add :% (x, Add :% (b, c))) (Add :% (Add :% (x, b), c))
forall f (k :: * -> * -> *) a b c.
(TensorProduct f, Cod f ~ k) =>
f
-> Obj k a
-> Obj k b
-> Obj k c
-> k (f :% (a, f :% (b, c))) (f :% (f :% (a, b), c))
associatorInv Add
Add Obj Cube x
Cube x y
l Obj k b
Obj Cube b
m Obj k c
Obj Cube c
n)