{-# LANGUAGE TypeFamilies, GADTs, RankNTypes, TypeOperators, UndecidableInstances, NoImplicitPrelude #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Category.Cube
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  sjoerd@w3future.com
-- Stability   :  experimental
-- Portability :  non-portable
--
-- The cube category.
-----------------------------------------------------------------------------
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) -- face maps
  X :: Cube x y -> Cube (S x) y -- degeneracy map


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
-- | Turn @Cube x y@ arrows into @ACube x -> ACube y@ functions.
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
-- | Ordinal addition is a bifuntor, it concattenates the maps as it were.
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)