{-# 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.Kind (Type)

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 :: Type -> Type -> Type 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 :: forall a b. Cube a b -> Obj Cube a
src Cube a b
Z = Cube Z Z
Z
  src (S Cube x y
c) = forall a1 b1. Cube a1 b1 -> Cube (S a1) (S b1)
S (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) = 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) = forall a1 b1. Cube a1 b1 -> Cube (S a1) (S b1)
S (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Cube x b
c)

  tgt :: forall a b. Cube a b -> Obj Cube b
tgt Cube a b
Z = Cube Z Z
Z
  tgt (S Cube x y
c) = forall a1 b1. Cube a1 b1 -> Cube (S a1) (S b1)
S (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) = forall a1 b1. Cube a1 b1 -> Cube (S a1) (S b1)
S (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) = 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 . :: forall b c a. Cube b c -> Cube a b -> Cube a c
. Cube a b
c = Cube a b
c
  Cube b c
c . Cube a b
Z = Cube b c
c
  S Cube x y
c . S Cube x y
d = forall a1 b1. Cube a1 b1 -> Cube (S a1) (S b1)
S (Cube x y
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 y
d)
  S Cube x y
c . Y Sign
s Cube a y
d = forall x a1. Sign -> Cube x a1 -> Cube x (S a1)
Y Sign
s (Cube x y
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 y
d)
  Y Sign
s Cube b y
c . Cube a b
d = forall x a1. Sign -> Cube x a1 -> Cube x (S a1)
Y Sign
s (Cube b y
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 b
d)
  X Cube x c
c . S Cube x y
d = forall a1 y. Cube a1 y -> Cube (S a1) y
X (Cube x c
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 y
d)
  X Cube x c
c . Y Sign
_ Cube a y
d = Cube x c
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 y
d
  Cube b c
c . X Cube x b
d = forall a1 y. Cube a1 y -> Cube (S a1) y
X (Cube b c
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 = Cube Z Z
Z

  terminate :: forall a. Obj Cube a -> Cube a (TerminalObject Cube)
terminate Cube a a
Z = Cube Z Z
Z
  terminate (S Cube x y
f) = forall a1 y. Cube a1 y -> Cube (S a1) y
X (forall {k} (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate Cube x y
f)


data Sign0 = SM | S0 | SP

data ACube :: Type -> Type 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 % :: forall a b.
Forget -> Dom Forget a b -> Cod Forget (Forget :% a) (Forget :% b)
% Dom Forget a b
Cube a b
Z     = \ACube Z
x -> ACube Z
x
  Forget
Forget % S Cube x y
f   = \(Cons Sign0
s ACube n
x) -> forall a1. Sign0 -> ACube a1 -> ACube (S a1)
Cons Sign0
s ((Forget
Forget forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Cube x y
f) ACube n
x)
  Forget
Forget % Y Sign
M Cube a y
f = \ACube a
x -> forall a1. Sign0 -> ACube a1 -> ACube (S a1)
Cons Sign0
SM ((Forget
Forget forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Cube a y
f) ACube a
x)
  Forget
Forget % Y Sign
P Cube a y
f = \ACube a
x -> forall a1. Sign0 -> ACube a1 -> ACube (S a1)
Cons Sign0
SP ((Forget
Forget forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Cube a y
f) ACube a
x)
  Forget
Forget % X Cube x b
f   = \(Cons Sign0
_ ACube n
x) -> (Forget
Forget forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% 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 % :: forall a b. Add -> Dom Add a b -> Cod Add (Add :% a) (Add :% b)
% (Cube a1 b1
Z     :**: Cube a2 b2
g) = Cube a2 b2
g
  Add
Add % (S Cube x y
f   :**: Cube a2 b2
g) = forall a1 b1. Cube a1 b1 -> Cube (S a1) (S b1)
S   (Add
Add forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (Cube x y
f 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 Sign
s Cube a1 y
f :**: Cube a2 b2
g) = forall x a1. Sign -> Cube x a1 -> Cube x (S a1)
Y Sign
s (Add
Add forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (Cube a1 y
f 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 Cube x b1
f   :**: Cube a2 b2
g) = forall a1 y. Cube a1 y -> Cube (S a1) y
X   (Add
Add forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (Cube x b1
f 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 = Cube Z Z
Z

  leftUnitor :: forall (k :: * -> * -> *) a.
(Cod Add ~ k) =>
Add -> Obj k a -> k (Add :% (Unit Add, a)) a
leftUnitor     Add
Add    Obj k a
a  = Obj k a
a
  leftUnitorInv :: forall (k :: * -> * -> *) a.
(Cod Add ~ k) =>
Add -> Obj k a -> k a (Add :% (Unit Add, a))
leftUnitorInv  Add
Add    Obj k a
a  = Obj k a
a
  rightUnitor :: forall (k :: * -> * -> *) a.
(Cod Add ~ k) =>
Add -> Obj k a -> k (Add :% (a, Unit Add)) a
rightUnitor    Add
Add    Obj k a
Cube a a
Z  = Cube Z Z
Z
  rightUnitor    Add
Add (S Cube x y
n) = forall a1 b1. Cube a1 b1 -> Cube (S a1) (S b1)
S (forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k (f :% (a, Unit f)) a
rightUnitor Add
Add Cube x y
n)
  rightUnitorInv :: forall (k :: * -> * -> *) a.
(Cod Add ~ k) =>
Add -> Obj k a -> k a (Add :% (a, Unit Add))
rightUnitorInv Add
Add    Obj k a
Cube a a
Z  = Cube Z Z
Z
  rightUnitorInv Add
Add (S Cube x y
n) = forall a1 b1. Cube a1 b1 -> Cube (S a1) (S b1)
S (forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k a (f :% (a, Unit f))
rightUnitorInv Add
Add Cube x y
n)
  associator :: forall (k :: * -> * -> *) a b c.
(Cod Add ~ k) =>
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
Cube a a
Z    Obj k b
Cube b b
Z  Obj k c
n = Obj k c
n
  associator     Add
Add Obj k a
Cube a a
Z (S Cube x y
m) Obj k c
n = forall a1 b1. Cube a1 b1 -> Cube (S a1) (S b1)
S (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 Cube x y
m Obj k c
n)
  associator     Add
Add (S Cube x y
l) Obj k b
m Obj k c
n = forall a1 b1. Cube a1 b1 -> Cube (S a1) (S b1)
S (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 x y
l Obj k b
m Obj k c
n)
  associatorInv :: forall (k :: * -> * -> *) a b c.
(Cod Add ~ k) =>
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
Cube a a
Z    Obj k b
Cube b b
Z  Obj k c
n = Obj k c
n
  associatorInv  Add
Add Obj k a
Cube a a
Z (S Cube x y
m) Obj k c
n = forall a1 b1. Cube a1 b1 -> Cube (S a1) (S b1)
S (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 Cube x y
m Obj k c
n)
  associatorInv  Add
Add (S Cube x y
l) Obj k b
m Obj k c
n = forall a1 b1. Cube a1 b1 -> Cube (S a1) (S b1)
S (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 x y
l Obj k b
m Obj k c
n)