-- Copyright (c) 2010-2014, David Amos. All rights reserved.

{-# LANGUAGE TypeFamilies, EmptyDataDecls, MultiParamTypeClasses #-}

-- |A module defining classes and example instances of categories, monoidal categories and braided categories
module Math.QuantumAlgebra.TensorCategory where

import Data.List as L

class MCategory c where
    data Ob c :: *
    data Ar c :: *
    id_ :: Ob c -> Ar c
    source, target :: Ar c -> Ob c
    (>>>) :: Ar c -> Ar c -> Ar c
-- Note that the class Category defined in Control.Category is about categories whose objects are Haskell types,
-- whereas we want the objects to be values of a single type.


class (MCategory a, MCategory b) => MFunctor a b where
    fob :: Ob a -> Ob b -- functor on objects
    far :: Ar a -> Ar b -- functor on arrows

-- We could also define tensor functors and braided functors, which are just functors which commute appropriately
-- with tensor and braiding operations


-- Kassel p282
-- The following is actually definition of a _strict_ monoidal category
-- Also called tensor category
class MCategory c => Monoidal c where
    tunit :: Ob c
    tob :: Ob c -> Ob c -> Ob c -- tensor product of objects
    tar :: Ar c -> Ar c -> Ar c -- tensor product of arrows

class Monoidal c => StrictMonoidal c where {}
-- we want to be able to declare some tensor categories as strict

class Monoidal c => WeakMonoidal c where
    assoc :: Ob c -> Ob c -> Ob c -> Ar c -- assoc u v w is an arrow (natural transformation?): (u `tob` v) `tob` w -> u `tob` (v `tob` w)
    lunit :: Ob c -> Ar c                 -- lunit v is an arrow (isomorphism): tunit `tob` v -> v
    runit :: Ob c -> Ar c                 -- runit v is an arrow (isomorphism): v `tob` tunit -> v

{-
instance (Monoidal c, Eq (Ar c), Show (Ar c)) => Num (Ar c) where
    (*) = tar
-}

class Monoidal c => Braided c where
    twist :: Ob c -> Ob c -> Ar c
    -- twist v w is a map from v tensor w to w tensor v
    -- twist must be natural, and satisfy certain commutative diagrams - Kock 161, 169

class Braided c => Symmetric c where {}
-- if twist satisfies twist v w >>> twist w v == id_ (v tensor w), then the category is symmetric


-- SIMPLEX CATEGORIES

-- Kock, Frobenius Algebras ..., p178-9
-- The skeleton of FinOrd (finite ordered sets)
-- The objects are the finite ordinals n == [0..n-1]
-- The arrows are the order-preserving maps
data FinOrd

instance MCategory FinOrd where
    data Ob FinOrd = FinOrdOb Int deriving (Ob FinOrd -> Ob FinOrd -> Bool
(Ob FinOrd -> Ob FinOrd -> Bool)
-> (Ob FinOrd -> Ob FinOrd -> Bool) -> Eq (Ob FinOrd)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Ob FinOrd -> Ob FinOrd -> Bool
$c/= :: Ob FinOrd -> Ob FinOrd -> Bool
== :: Ob FinOrd -> Ob FinOrd -> Bool
$c== :: Ob FinOrd -> Ob FinOrd -> Bool
Eq,Eq (Ob FinOrd)
Eq (Ob FinOrd) =>
(Ob FinOrd -> Ob FinOrd -> Ordering)
-> (Ob FinOrd -> Ob FinOrd -> Bool)
-> (Ob FinOrd -> Ob FinOrd -> Bool)
-> (Ob FinOrd -> Ob FinOrd -> Bool)
-> (Ob FinOrd -> Ob FinOrd -> Bool)
-> (Ob FinOrd -> Ob FinOrd -> Ob FinOrd)
-> (Ob FinOrd -> Ob FinOrd -> Ob FinOrd)
-> Ord (Ob FinOrd)
Ob FinOrd -> Ob FinOrd -> Bool
Ob FinOrd -> Ob FinOrd -> Ordering
Ob FinOrd -> Ob FinOrd -> Ob FinOrd
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Ob FinOrd -> Ob FinOrd -> Ob FinOrd
$cmin :: Ob FinOrd -> Ob FinOrd -> Ob FinOrd
max :: Ob FinOrd -> Ob FinOrd -> Ob FinOrd
$cmax :: Ob FinOrd -> Ob FinOrd -> Ob FinOrd
>= :: Ob FinOrd -> Ob FinOrd -> Bool
$c>= :: Ob FinOrd -> Ob FinOrd -> Bool
> :: Ob FinOrd -> Ob FinOrd -> Bool
$c> :: Ob FinOrd -> Ob FinOrd -> Bool
<= :: Ob FinOrd -> Ob FinOrd -> Bool
$c<= :: Ob FinOrd -> Ob FinOrd -> Bool
< :: Ob FinOrd -> Ob FinOrd -> Bool
$c< :: Ob FinOrd -> Ob FinOrd -> Bool
compare :: Ob FinOrd -> Ob FinOrd -> Ordering
$ccompare :: Ob FinOrd -> Ob FinOrd -> Ordering
$cp1Ord :: Eq (Ob FinOrd)
Ord,Int -> Ob FinOrd -> ShowS
[Ob FinOrd] -> ShowS
Ob FinOrd -> String
(Int -> Ob FinOrd -> ShowS)
-> (Ob FinOrd -> String)
-> ([Ob FinOrd] -> ShowS)
-> Show (Ob FinOrd)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Ob FinOrd] -> ShowS
$cshowList :: [Ob FinOrd] -> ShowS
show :: Ob FinOrd -> String
$cshow :: Ob FinOrd -> String
showsPrec :: Int -> Ob FinOrd -> ShowS
$cshowsPrec :: Int -> Ob FinOrd -> ShowS
Show)
    -- FinOrdOb n represents the oriented simplex n == [0..n-1]
    data Ar FinOrd = FinOrdAr Int Int [Int] deriving (Ar FinOrd -> Ar FinOrd -> Bool
(Ar FinOrd -> Ar FinOrd -> Bool)
-> (Ar FinOrd -> Ar FinOrd -> Bool) -> Eq (Ar FinOrd)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Ar FinOrd -> Ar FinOrd -> Bool
$c/= :: Ar FinOrd -> Ar FinOrd -> Bool
== :: Ar FinOrd -> Ar FinOrd -> Bool
$c== :: Ar FinOrd -> Ar FinOrd -> Bool
Eq,Eq (Ar FinOrd)
Eq (Ar FinOrd) =>
(Ar FinOrd -> Ar FinOrd -> Ordering)
-> (Ar FinOrd -> Ar FinOrd -> Bool)
-> (Ar FinOrd -> Ar FinOrd -> Bool)
-> (Ar FinOrd -> Ar FinOrd -> Bool)
-> (Ar FinOrd -> Ar FinOrd -> Bool)
-> (Ar FinOrd -> Ar FinOrd -> Ar FinOrd)
-> (Ar FinOrd -> Ar FinOrd -> Ar FinOrd)
-> Ord (Ar FinOrd)
Ar FinOrd -> Ar FinOrd -> Bool
Ar FinOrd -> Ar FinOrd -> Ordering
Ar FinOrd -> Ar FinOrd -> Ar FinOrd
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Ar FinOrd -> Ar FinOrd -> Ar FinOrd
$cmin :: Ar FinOrd -> Ar FinOrd -> Ar FinOrd
max :: Ar FinOrd -> Ar FinOrd -> Ar FinOrd
$cmax :: Ar FinOrd -> Ar FinOrd -> Ar FinOrd
>= :: Ar FinOrd -> Ar FinOrd -> Bool
$c>= :: Ar FinOrd -> Ar FinOrd -> Bool
> :: Ar FinOrd -> Ar FinOrd -> Bool
$c> :: Ar FinOrd -> Ar FinOrd -> Bool
<= :: Ar FinOrd -> Ar FinOrd -> Bool
$c<= :: Ar FinOrd -> Ar FinOrd -> Bool
< :: Ar FinOrd -> Ar FinOrd -> Bool
$c< :: Ar FinOrd -> Ar FinOrd -> Bool
compare :: Ar FinOrd -> Ar FinOrd -> Ordering
$ccompare :: Ar FinOrd -> Ar FinOrd -> Ordering
$cp1Ord :: Eq (Ar FinOrd)
Ord,Int -> Ar FinOrd -> ShowS
[Ar FinOrd] -> ShowS
Ar FinOrd -> String
(Int -> Ar FinOrd -> ShowS)
-> (Ar FinOrd -> String)
-> ([Ar FinOrd] -> ShowS)
-> Show (Ar FinOrd)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Ar FinOrd] -> ShowS
$cshowList :: [Ar FinOrd] -> ShowS
show :: Ar FinOrd -> String
$cshow :: Ar FinOrd -> String
showsPrec :: Int -> Ar FinOrd -> ShowS
$cshowsPrec :: Int -> Ar FinOrd -> ShowS
Show)
    -- FinOrdAr s t fs represents the order-preserving map, zip [0..s-1] fs.
    -- For example FinOrdAr 3 2 [0,0,1] represents the map 0 -> 0, 1 -> 0, 2 -> 1
    id_ :: Ob FinOrd -> Ar FinOrd
id_ (FinOrdOb n) = Int -> Int -> [Int] -> Ar FinOrd
FinOrdAr Int
n Int
n [0..Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-1]
    source :: Ar FinOrd -> Ob FinOrd
source (FinOrdAr s _ _) = Int -> Ob FinOrd
FinOrdOb Int
s
    target :: Ar FinOrd -> Ob FinOrd
target (FinOrdAr _ t _) = Int -> Ob FinOrd
FinOrdOb Int
t
    FinOrdAr sf tf fs >>> :: Ar FinOrd -> Ar FinOrd -> Ar FinOrd
>>> FinOrdAr sg tg gs | Int
tf Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
sg = Int -> Int -> [Int] -> Ar FinOrd
FinOrdAr Int
sf Int
tg [let j :: Int
j = [Int]
fs [Int] -> Int -> Int
forall a. [a] -> Int -> a
!! Int
i in [Int]
gs [Int] -> Int -> Int
forall a. [a] -> Int -> a
!! Int
j | Int
i <- [0..Int
sfInt -> Int -> Int
forall a. Num a => a -> a -> a
-1] ]

instance Monoidal FinOrd where
    tunit :: Ob FinOrd
tunit = Int -> Ob FinOrd
FinOrdOb 0
    tob :: Ob FinOrd -> Ob FinOrd -> Ob FinOrd
tob (FinOrdOb m) (FinOrdOb n) = Int -> Ob FinOrd
FinOrdOb (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
n)
    tar :: Ar FinOrd -> Ar FinOrd -> Ar FinOrd
tar (FinOrdAr sf tf fs) (FinOrdAr sg tg gs) = Int -> Int -> [Int] -> Ar FinOrd
FinOrdAr (Int
sfInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
sg) (Int
tfInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
tg) ([Int]
fs [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ (Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
tf) [Int]
gs)

finOrdAr :: Int -> Int -> [Int] -> Ar FinOrd
finOrdAr s :: Int
s t :: Int
t fs :: [Int]
fs | Int
s Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
fs Bool -> Bool -> Bool
&& [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [Int]
fs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 0 Bool -> Bool -> Bool
&& [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Int]
fs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
t Bool -> Bool -> Bool
&& [Int] -> Bool
forall a. Ord a => [a] -> Bool
isOrderPreserving [Int]
fs
    = Int -> Int -> [Int] -> Ar FinOrd
FinOrdAr Int
s Int
t [Int]
fs
    where isOrderPreserving :: [a] -> Bool
isOrderPreserving (f1 :: a
f1:f2 :: a
f2:fs :: [a]
fs) = a
f1 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
f2 Bool -> Bool -> Bool
&& [a] -> Bool
isOrderPreserving (a
f2a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
fs)
          isOrderPreserving _ = Bool
True


-- The skeleton of FinSet
-- The objects are the finite cardinals n == {0..n-1} (with no order)
-- The arrows are the maps
data FinCard

instance MCategory FinCard where
    data Ob FinCard = FinCardOb Int deriving (Ob FinCard -> Ob FinCard -> Bool
(Ob FinCard -> Ob FinCard -> Bool)
-> (Ob FinCard -> Ob FinCard -> Bool) -> Eq (Ob FinCard)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Ob FinCard -> Ob FinCard -> Bool
$c/= :: Ob FinCard -> Ob FinCard -> Bool
== :: Ob FinCard -> Ob FinCard -> Bool
$c== :: Ob FinCard -> Ob FinCard -> Bool
Eq,Eq (Ob FinCard)
Eq (Ob FinCard) =>
(Ob FinCard -> Ob FinCard -> Ordering)
-> (Ob FinCard -> Ob FinCard -> Bool)
-> (Ob FinCard -> Ob FinCard -> Bool)
-> (Ob FinCard -> Ob FinCard -> Bool)
-> (Ob FinCard -> Ob FinCard -> Bool)
-> (Ob FinCard -> Ob FinCard -> Ob FinCard)
-> (Ob FinCard -> Ob FinCard -> Ob FinCard)
-> Ord (Ob FinCard)
Ob FinCard -> Ob FinCard -> Bool
Ob FinCard -> Ob FinCard -> Ordering
Ob FinCard -> Ob FinCard -> Ob FinCard
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Ob FinCard -> Ob FinCard -> Ob FinCard
$cmin :: Ob FinCard -> Ob FinCard -> Ob FinCard
max :: Ob FinCard -> Ob FinCard -> Ob FinCard
$cmax :: Ob FinCard -> Ob FinCard -> Ob FinCard
>= :: Ob FinCard -> Ob FinCard -> Bool
$c>= :: Ob FinCard -> Ob FinCard -> Bool
> :: Ob FinCard -> Ob FinCard -> Bool
$c> :: Ob FinCard -> Ob FinCard -> Bool
<= :: Ob FinCard -> Ob FinCard -> Bool
$c<= :: Ob FinCard -> Ob FinCard -> Bool
< :: Ob FinCard -> Ob FinCard -> Bool
$c< :: Ob FinCard -> Ob FinCard -> Bool
compare :: Ob FinCard -> Ob FinCard -> Ordering
$ccompare :: Ob FinCard -> Ob FinCard -> Ordering
$cp1Ord :: Eq (Ob FinCard)
Ord,Int -> Ob FinCard -> ShowS
[Ob FinCard] -> ShowS
Ob FinCard -> String
(Int -> Ob FinCard -> ShowS)
-> (Ob FinCard -> String)
-> ([Ob FinCard] -> ShowS)
-> Show (Ob FinCard)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Ob FinCard] -> ShowS
$cshowList :: [Ob FinCard] -> ShowS
show :: Ob FinCard -> String
$cshow :: Ob FinCard -> String
showsPrec :: Int -> Ob FinCard -> ShowS
$cshowsPrec :: Int -> Ob FinCard -> ShowS
Show)
    -- FinCardOb n represents the unoriented simplex n == {0..n-1}
    data Ar FinCard = FinCardAr Int Int [Int] deriving (Ar FinCard -> Ar FinCard -> Bool
(Ar FinCard -> Ar FinCard -> Bool)
-> (Ar FinCard -> Ar FinCard -> Bool) -> Eq (Ar FinCard)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Ar FinCard -> Ar FinCard -> Bool
$c/= :: Ar FinCard -> Ar FinCard -> Bool
== :: Ar FinCard -> Ar FinCard -> Bool
$c== :: Ar FinCard -> Ar FinCard -> Bool
Eq,Eq (Ar FinCard)
Eq (Ar FinCard) =>
(Ar FinCard -> Ar FinCard -> Ordering)
-> (Ar FinCard -> Ar FinCard -> Bool)
-> (Ar FinCard -> Ar FinCard -> Bool)
-> (Ar FinCard -> Ar FinCard -> Bool)
-> (Ar FinCard -> Ar FinCard -> Bool)
-> (Ar FinCard -> Ar FinCard -> Ar FinCard)
-> (Ar FinCard -> Ar FinCard -> Ar FinCard)
-> Ord (Ar FinCard)
Ar FinCard -> Ar FinCard -> Bool
Ar FinCard -> Ar FinCard -> Ordering
Ar FinCard -> Ar FinCard -> Ar FinCard
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Ar FinCard -> Ar FinCard -> Ar FinCard
$cmin :: Ar FinCard -> Ar FinCard -> Ar FinCard
max :: Ar FinCard -> Ar FinCard -> Ar FinCard
$cmax :: Ar FinCard -> Ar FinCard -> Ar FinCard
>= :: Ar FinCard -> Ar FinCard -> Bool
$c>= :: Ar FinCard -> Ar FinCard -> Bool
> :: Ar FinCard -> Ar FinCard -> Bool
$c> :: Ar FinCard -> Ar FinCard -> Bool
<= :: Ar FinCard -> Ar FinCard -> Bool
$c<= :: Ar FinCard -> Ar FinCard -> Bool
< :: Ar FinCard -> Ar FinCard -> Bool
$c< :: Ar FinCard -> Ar FinCard -> Bool
compare :: Ar FinCard -> Ar FinCard -> Ordering
$ccompare :: Ar FinCard -> Ar FinCard -> Ordering
$cp1Ord :: Eq (Ar FinCard)
Ord,Int -> Ar FinCard -> ShowS
[Ar FinCard] -> ShowS
Ar FinCard -> String
(Int -> Ar FinCard -> ShowS)
-> (Ar FinCard -> String)
-> ([Ar FinCard] -> ShowS)
-> Show (Ar FinCard)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Ar FinCard] -> ShowS
$cshowList :: [Ar FinCard] -> ShowS
show :: Ar FinCard -> String
$cshow :: Ar FinCard -> String
showsPrec :: Int -> Ar FinCard -> ShowS
$cshowsPrec :: Int -> Ar FinCard -> ShowS
Show)
    -- FinCardAr s t fs represents the map, zip [0..s-1] fs.
    -- For example FinCardAr 3 2 [0,1,0] represents the map 0 -> 0, 1 -> 1, 2 -> 0
    id_ :: Ob FinCard -> Ar FinCard
id_ (FinCardOb n) = Int -> Int -> [Int] -> Ar FinCard
FinCardAr Int
n Int
n [0..Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-1]
    source :: Ar FinCard -> Ob FinCard
source (FinCardAr s _ _) = Int -> Ob FinCard
FinCardOb Int
s
    target :: Ar FinCard -> Ob FinCard
target (FinCardAr _ t _) = Int -> Ob FinCard
FinCardOb Int
t
    FinCardAr sf tf fs >>> :: Ar FinCard -> Ar FinCard -> Ar FinCard
>>> FinCardAr sg tg gs | Int
tf Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
sg = Int -> Int -> [Int] -> Ar FinCard
FinCardAr Int
sf Int
tg [let j :: Int
j = [Int]
fs [Int] -> Int -> Int
forall a. [a] -> Int -> a
!! Int
i in [Int]
gs [Int] -> Int -> Int
forall a. [a] -> Int -> a
!! Int
j | Int
i <- [0..Int
sfInt -> Int -> Int
forall a. Num a => a -> a -> a
-1] ]

instance Monoidal FinCard where
    tunit :: Ob FinCard
tunit = Int -> Ob FinCard
FinCardOb 0
    tob :: Ob FinCard -> Ob FinCard -> Ob FinCard
tob (FinCardOb m) (FinCardOb n) = Int -> Ob FinCard
FinCardOb (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
n)
    tar :: Ar FinCard -> Ar FinCard -> Ar FinCard
tar (FinCardAr sf tf fs) (FinCardAr sg tg gs) = Int -> Int -> [Int] -> Ar FinCard
FinCardAr (Int
sfInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
sg) (Int
tfInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
tg) ([Int]
fs [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ (Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
tf) [Int]
gs)

finCardAr :: Int -> Int -> [Int] -> Ar FinCard
finCardAr s :: Int
s t :: Int
t fs :: [Int]
fs | Int
s Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
fs Bool -> Bool -> Bool
&& [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [Int]
fs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 0 Bool -> Bool -> Bool
&& [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Int]
fs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
t -- for finite cardinals, the map doesn't have to be order-preserving
    = Int -> Int -> [Int] -> Ar FinCard
FinCardAr Int
s Int
t [Int]
fs

-- Finite permutations form a subcategory of FinCard
-- having as objects the finite cardinals n == {0..n-1}
-- and as arrows the bijections (== permutations)
finPerm :: [Int] -> Ar FinCard
finPerm fs :: [Int]
fs | [Int] -> [Int]
forall a. Ord a => [a] -> [a]
L.sort [Int]
fs [Int] -> [Int] -> Bool
forall a. Eq a => a -> a -> Bool
== [0..Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-1] = Int -> Int -> [Int] -> Ar FinCard
FinCardAr Int
n Int
n [Int]
fs
    where n :: Int
n = [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
fs
-- (Note that these are permutations of [0..n-1], rather than [1..n])


-- This is the forgetful functor FinOrd -> FinCard (FinSet)
instance MFunctor FinOrd FinCard where
    fob :: Ob FinOrd -> Ob FinCard
fob (FinOrdOb n) = Int -> Ob FinCard
FinCardOb Int
n
    far :: Ar FinOrd -> Ar FinCard
far (FinOrdAr s t fs) = Int -> Int -> [Int] -> Ar FinCard
FinCardAr Int
s Int
t [Int]
fs


-- BRAID CATEGORY

data Braid

instance MCategory Braid where
    data Ob Braid = BraidOb Int deriving (Ob Braid -> Ob Braid -> Bool
(Ob Braid -> Ob Braid -> Bool)
-> (Ob Braid -> Ob Braid -> Bool) -> Eq (Ob Braid)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Ob Braid -> Ob Braid -> Bool
$c/= :: Ob Braid -> Ob Braid -> Bool
== :: Ob Braid -> Ob Braid -> Bool
$c== :: Ob Braid -> Ob Braid -> Bool
Eq,Eq (Ob Braid)
Eq (Ob Braid) =>
(Ob Braid -> Ob Braid -> Ordering)
-> (Ob Braid -> Ob Braid -> Bool)
-> (Ob Braid -> Ob Braid -> Bool)
-> (Ob Braid -> Ob Braid -> Bool)
-> (Ob Braid -> Ob Braid -> Bool)
-> (Ob Braid -> Ob Braid -> Ob Braid)
-> (Ob Braid -> Ob Braid -> Ob Braid)
-> Ord (Ob Braid)
Ob Braid -> Ob Braid -> Bool
Ob Braid -> Ob Braid -> Ordering
Ob Braid -> Ob Braid -> Ob Braid
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Ob Braid -> Ob Braid -> Ob Braid
$cmin :: Ob Braid -> Ob Braid -> Ob Braid
max :: Ob Braid -> Ob Braid -> Ob Braid
$cmax :: Ob Braid -> Ob Braid -> Ob Braid
>= :: Ob Braid -> Ob Braid -> Bool
$c>= :: Ob Braid -> Ob Braid -> Bool
> :: Ob Braid -> Ob Braid -> Bool
$c> :: Ob Braid -> Ob Braid -> Bool
<= :: Ob Braid -> Ob Braid -> Bool
$c<= :: Ob Braid -> Ob Braid -> Bool
< :: Ob Braid -> Ob Braid -> Bool
$c< :: Ob Braid -> Ob Braid -> Bool
compare :: Ob Braid -> Ob Braid -> Ordering
$ccompare :: Ob Braid -> Ob Braid -> Ordering
$cp1Ord :: Eq (Ob Braid)
Ord,Int -> Ob Braid -> ShowS
[Ob Braid] -> ShowS
Ob Braid -> String
(Int -> Ob Braid -> ShowS)
-> (Ob Braid -> String) -> ([Ob Braid] -> ShowS) -> Show (Ob Braid)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Ob Braid] -> ShowS
$cshowList :: [Ob Braid] -> ShowS
show :: Ob Braid -> String
$cshow :: Ob Braid -> String
showsPrec :: Int -> Ob Braid -> ShowS
$cshowsPrec :: Int -> Ob Braid -> ShowS
Show)
    data Ar Braid = BraidAr Int [Int] deriving (Ar Braid -> Ar Braid -> Bool
(Ar Braid -> Ar Braid -> Bool)
-> (Ar Braid -> Ar Braid -> Bool) -> Eq (Ar Braid)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Ar Braid -> Ar Braid -> Bool
$c/= :: Ar Braid -> Ar Braid -> Bool
== :: Ar Braid -> Ar Braid -> Bool
$c== :: Ar Braid -> Ar Braid -> Bool
Eq,Eq (Ar Braid)
Eq (Ar Braid) =>
(Ar Braid -> Ar Braid -> Ordering)
-> (Ar Braid -> Ar Braid -> Bool)
-> (Ar Braid -> Ar Braid -> Bool)
-> (Ar Braid -> Ar Braid -> Bool)
-> (Ar Braid -> Ar Braid -> Bool)
-> (Ar Braid -> Ar Braid -> Ar Braid)
-> (Ar Braid -> Ar Braid -> Ar Braid)
-> Ord (Ar Braid)
Ar Braid -> Ar Braid -> Bool
Ar Braid -> Ar Braid -> Ordering
Ar Braid -> Ar Braid -> Ar Braid
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Ar Braid -> Ar Braid -> Ar Braid
$cmin :: Ar Braid -> Ar Braid -> Ar Braid
max :: Ar Braid -> Ar Braid -> Ar Braid
$cmax :: Ar Braid -> Ar Braid -> Ar Braid
>= :: Ar Braid -> Ar Braid -> Bool
$c>= :: Ar Braid -> Ar Braid -> Bool
> :: Ar Braid -> Ar Braid -> Bool
$c> :: Ar Braid -> Ar Braid -> Bool
<= :: Ar Braid -> Ar Braid -> Bool
$c<= :: Ar Braid -> Ar Braid -> Bool
< :: Ar Braid -> Ar Braid -> Bool
$c< :: Ar Braid -> Ar Braid -> Bool
compare :: Ar Braid -> Ar Braid -> Ordering
$ccompare :: Ar Braid -> Ar Braid -> Ordering
$cp1Ord :: Eq (Ar Braid)
Ord,Int -> Ar Braid -> ShowS
[Ar Braid] -> ShowS
Ar Braid -> String
(Int -> Ar Braid -> ShowS)
-> (Ar Braid -> String) -> ([Ar Braid] -> ShowS) -> Show (Ar Braid)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Ar Braid] -> ShowS
$cshowList :: [Ar Braid] -> ShowS
show :: Ar Braid -> String
$cshow :: Ar Braid -> String
showsPrec :: Int -> Ar Braid -> ShowS
$cshowsPrec :: Int -> Ar Braid -> ShowS
Show)
    id_ :: Ob Braid -> Ar Braid
id_ (BraidOb n) = Int -> [Int] -> Ar Braid
BraidAr Int
n []
    source :: Ar Braid -> Ob Braid
source (BraidAr n _) = Int -> Ob Braid
BraidOb Int
n
    target :: Ar Braid -> Ob Braid
target (BraidAr n _) = Int -> Ob Braid
BraidOb Int
n
    BraidAr m is >>> :: Ar Braid -> Ar Braid -> Ar Braid
>>> BraidAr n js | Int
m Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n = Int -> [Int] -> Ar Braid
BraidAr Int
m ([Int] -> [Int] -> [Int]
forall a. (Eq a, Num a) => [a] -> [a] -> [a]
cancel ([Int] -> [Int]
forall a. [a] -> [a]
reverse [Int]
is) [Int]
js)
        where cancel :: [a] -> [a] -> [a]
cancel (x :: a
x:xs :: [a]
xs) (y :: a
y:ys :: [a]
ys) = if a
xa -> a -> a
forall a. Num a => a -> a -> a
+a
y a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== 0 then [a] -> [a] -> [a]
cancel [a]
xs [a]
ys else [a] -> [a]
forall a. [a] -> [a]
reverse [a]
xs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:a
ya -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ys
              cancel xs :: [a]
xs ys :: [a]
ys = [a] -> [a]
forall a. [a] -> [a]
reverse [a]
xs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
ys

t :: Int -> Int -> Ar Braid
t n :: Int
n 0 = Int -> [Int] -> Ar Braid
BraidAr Int
n [] -- the identity braid
t n :: Int
n i :: Int
i |  0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
i Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n = Int -> [Int] -> Ar Braid
BraidAr Int
n [Int
i]
      | -Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
i Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0 = Int -> [Int] -> Ar Braid
BraidAr Int
n [Int
i]
-- The generators of B_n are [t n i | i <- [1..n-1]]

-- The inverses of the braid generators
t' :: Int -> Int -> Ar Braid
t' n :: Int
n i :: Int
i | 0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
i Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n = Int -> [Int] -> Ar Braid
BraidAr Int
n [-Int
i]

instance Monoidal Braid where
    tunit :: Ob Braid
tunit = Int -> Ob Braid
BraidOb 0
    tob :: Ob Braid -> Ob Braid -> Ob Braid
tob (BraidOb m) (BraidOb n) = Int -> Ob Braid
BraidOb (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
n)
    tar :: Ar Braid -> Ar Braid -> Ar Braid
tar (BraidAr m is) (BraidAr n js) = Int -> [Int] -> Ar Braid
BraidAr (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
n) ([Int]
is [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ (Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
m) [Int]
js)

instance Braided Braid where
    twist :: Ob Braid -> Ob Braid -> Ar Braid
twist (BraidOb m) (BraidOb n) = Int -> [Int] -> Ar Braid
BraidAr (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
n) ([Int] -> Ar Braid) -> [Int] -> Ar Braid
forall a b. (a -> b) -> a -> b
$ [[Int]] -> [Int]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Int
i..Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-1] | Int
i <- [Int
m,Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-1..1]]

-- Note that in FinCard we consider the objects as [0..n-1], whereas in Braid we consider them as [1..n], so that s_i twists [i,i+1]
instance MFunctor Braid FinCard where
    fob :: Ob Braid -> Ob FinCard
fob (BraidOb n) = Int -> Ob FinCard
FinCardOb Int
n
    far :: Ar Braid -> Ar FinCard
far (BraidAr n ss) = (Ar FinCard -> Ar FinCard -> Ar FinCard)
-> Ar FinCard -> [Ar FinCard] -> Ar FinCard
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ar FinCard -> Ar FinCard -> Ar FinCard
forall c. MCategory c => Ar c -> Ar c -> Ar c
(>>>) (Ob FinCard -> Ar FinCard
forall c. MCategory c => Ob c -> Ar c
id_ (Int -> Ob FinCard
FinCardOb Int
n)) [[Int] -> Ar FinCard
finPerm ([0..Int
tiInt -> Int -> Int
forall a. Num a => a -> a -> a
-1] [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int
tiInt -> Int -> Int
forall a. Num a => a -> a -> a
+1,Int
ti] [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int
tiInt -> Int -> Int
forall a. Num a => a -> a -> a
+2..Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-1]) | Int
si <- [Int]
ss, let ti :: Int
ti = Int -> Int
forall a. Num a => a -> a
abs Int
si Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1]


-- VECT

data Vect k

instance Num k => MCategory (Vect k) where
    data Ob (Vect k) = VectOb Int deriving (Ob (Vect k) -> Ob (Vect k) -> Bool
(Ob (Vect k) -> Ob (Vect k) -> Bool)
-> (Ob (Vect k) -> Ob (Vect k) -> Bool) -> Eq (Ob (Vect k))
forall k. Ob (Vect k) -> Ob (Vect k) -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Ob (Vect k) -> Ob (Vect k) -> Bool
$c/= :: forall k. Ob (Vect k) -> Ob (Vect k) -> Bool
== :: Ob (Vect k) -> Ob (Vect k) -> Bool
$c== :: forall k. Ob (Vect k) -> Ob (Vect k) -> Bool
Eq,Eq (Ob (Vect k))
Eq (Ob (Vect k)) =>
(Ob (Vect k) -> Ob (Vect k) -> Ordering)
-> (Ob (Vect k) -> Ob (Vect k) -> Bool)
-> (Ob (Vect k) -> Ob (Vect k) -> Bool)
-> (Ob (Vect k) -> Ob (Vect k) -> Bool)
-> (Ob (Vect k) -> Ob (Vect k) -> Bool)
-> (Ob (Vect k) -> Ob (Vect k) -> Ob (Vect k))
-> (Ob (Vect k) -> Ob (Vect k) -> Ob (Vect k))
-> Ord (Ob (Vect k))
Ob (Vect k) -> Ob (Vect k) -> Bool
Ob (Vect k) -> Ob (Vect k) -> Ordering
Ob (Vect k) -> Ob (Vect k) -> Ob (Vect k)
forall k. Eq (Ob (Vect k))
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k. Ob (Vect k) -> Ob (Vect k) -> Bool
forall k. Ob (Vect k) -> Ob (Vect k) -> Ordering
forall k. Ob (Vect k) -> Ob (Vect k) -> Ob (Vect k)
min :: Ob (Vect k) -> Ob (Vect k) -> Ob (Vect k)
$cmin :: forall k. Ob (Vect k) -> Ob (Vect k) -> Ob (Vect k)
max :: Ob (Vect k) -> Ob (Vect k) -> Ob (Vect k)
$cmax :: forall k. Ob (Vect k) -> Ob (Vect k) -> Ob (Vect k)
>= :: Ob (Vect k) -> Ob (Vect k) -> Bool
$c>= :: forall k. Ob (Vect k) -> Ob (Vect k) -> Bool
> :: Ob (Vect k) -> Ob (Vect k) -> Bool
$c> :: forall k. Ob (Vect k) -> Ob (Vect k) -> Bool
<= :: Ob (Vect k) -> Ob (Vect k) -> Bool
$c<= :: forall k. Ob (Vect k) -> Ob (Vect k) -> Bool
< :: Ob (Vect k) -> Ob (Vect k) -> Bool
$c< :: forall k. Ob (Vect k) -> Ob (Vect k) -> Bool
compare :: Ob (Vect k) -> Ob (Vect k) -> Ordering
$ccompare :: forall k. Ob (Vect k) -> Ob (Vect k) -> Ordering
$cp1Ord :: forall k. Eq (Ob (Vect k))
Ord,Int -> Ob (Vect k) -> ShowS
[Ob (Vect k)] -> ShowS
Ob (Vect k) -> String
(Int -> Ob (Vect k) -> ShowS)
-> (Ob (Vect k) -> String)
-> ([Ob (Vect k)] -> ShowS)
-> Show (Ob (Vect k))
forall k. Int -> Ob (Vect k) -> ShowS
forall k. [Ob (Vect k)] -> ShowS
forall k. Ob (Vect k) -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Ob (Vect k)] -> ShowS
$cshowList :: forall k. [Ob (Vect k)] -> ShowS
show :: Ob (Vect k) -> String
$cshow :: forall k. Ob (Vect k) -> String
showsPrec :: Int -> Ob (Vect k) -> ShowS
$cshowsPrec :: forall k. Int -> Ob (Vect k) -> ShowS
Show)
    data Ar (Vect k) = VectAr Int Int [[Int]] deriving (Ar (Vect k) -> Ar (Vect k) -> Bool
(Ar (Vect k) -> Ar (Vect k) -> Bool)
-> (Ar (Vect k) -> Ar (Vect k) -> Bool) -> Eq (Ar (Vect k))
forall k. Ar (Vect k) -> Ar (Vect k) -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Ar (Vect k) -> Ar (Vect k) -> Bool
$c/= :: forall k. Ar (Vect k) -> Ar (Vect k) -> Bool
== :: Ar (Vect k) -> Ar (Vect k) -> Bool
$c== :: forall k. Ar (Vect k) -> Ar (Vect k) -> Bool
Eq,Eq (Ar (Vect k))
Eq (Ar (Vect k)) =>
(Ar (Vect k) -> Ar (Vect k) -> Ordering)
-> (Ar (Vect k) -> Ar (Vect k) -> Bool)
-> (Ar (Vect k) -> Ar (Vect k) -> Bool)
-> (Ar (Vect k) -> Ar (Vect k) -> Bool)
-> (Ar (Vect k) -> Ar (Vect k) -> Bool)
-> (Ar (Vect k) -> Ar (Vect k) -> Ar (Vect k))
-> (Ar (Vect k) -> Ar (Vect k) -> Ar (Vect k))
-> Ord (Ar (Vect k))
Ar (Vect k) -> Ar (Vect k) -> Bool
Ar (Vect k) -> Ar (Vect k) -> Ordering
Ar (Vect k) -> Ar (Vect k) -> Ar (Vect k)
forall k. Eq (Ar (Vect k))
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k. Ar (Vect k) -> Ar (Vect k) -> Bool
forall k. Ar (Vect k) -> Ar (Vect k) -> Ordering
forall k. Ar (Vect k) -> Ar (Vect k) -> Ar (Vect k)
min :: Ar (Vect k) -> Ar (Vect k) -> Ar (Vect k)
$cmin :: forall k. Ar (Vect k) -> Ar (Vect k) -> Ar (Vect k)
max :: Ar (Vect k) -> Ar (Vect k) -> Ar (Vect k)
$cmax :: forall k. Ar (Vect k) -> Ar (Vect k) -> Ar (Vect k)
>= :: Ar (Vect k) -> Ar (Vect k) -> Bool
$c>= :: forall k. Ar (Vect k) -> Ar (Vect k) -> Bool
> :: Ar (Vect k) -> Ar (Vect k) -> Bool
$c> :: forall k. Ar (Vect k) -> Ar (Vect k) -> Bool
<= :: Ar (Vect k) -> Ar (Vect k) -> Bool
$c<= :: forall k. Ar (Vect k) -> Ar (Vect k) -> Bool
< :: Ar (Vect k) -> Ar (Vect k) -> Bool
$c< :: forall k. Ar (Vect k) -> Ar (Vect k) -> Bool
compare :: Ar (Vect k) -> Ar (Vect k) -> Ordering
$ccompare :: forall k. Ar (Vect k) -> Ar (Vect k) -> Ordering
$cp1Ord :: forall k. Eq (Ar (Vect k))
Ord,Int -> Ar (Vect k) -> ShowS
[Ar (Vect k)] -> ShowS
Ar (Vect k) -> String
(Int -> Ar (Vect k) -> ShowS)
-> (Ar (Vect k) -> String)
-> ([Ar (Vect k)] -> ShowS)
-> Show (Ar (Vect k))
forall k. Int -> Ar (Vect k) -> ShowS
forall k. [Ar (Vect k)] -> ShowS
forall k. Ar (Vect k) -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Ar (Vect k)] -> ShowS
$cshowList :: forall k. [Ar (Vect k)] -> ShowS
show :: Ar (Vect k) -> String
$cshow :: forall k. Ar (Vect k) -> String
showsPrec :: Int -> Ar (Vect k) -> ShowS
$cshowsPrec :: forall k. Int -> Ar (Vect k) -> ShowS
Show)
    id_ :: Ob (Vect k) -> Ar (Vect k)
id_ (VectOb n) = Int -> Int -> [[Int]] -> Ar (Vect k)
forall k. Int -> Int -> [[Int]] -> Ar (Vect k)
VectAr Int
n Int
n [[Int]]
idMx where idMx :: [[Int]]
idMx = [[if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j then 1 else 0 | Int
j <- [1..Int
n]] | Int
i <- [1..Int
n]]
    source :: Ar (Vect k) -> Ob (Vect k)
source (VectAr m _ _) = Int -> Ob (Vect k)
forall k. Int -> Ob (Vect k)
VectOb Int
m
    target :: Ar (Vect k) -> Ob (Vect k)
target (VectAr _ n _) = Int -> Ob (Vect k)
forall k. Int -> Ob (Vect k)
VectOb Int
n
    VectAr r c xss >>> :: Ar (Vect k) -> Ar (Vect k) -> Ar (Vect k)
>>> VectAr r' c' yss | Int
c Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
r' = Ar (Vect k)
forall a. HasCallStack => a
undefined -- matrix multiplication

-- functor from FinPerm to Vect k


-- 2-COBORDISMS

data Cob2
-- works very similar to Tangle category

instance MCategory Cob2 where
    data Ob Cob2 = O Int deriving (Ob Cob2 -> Ob Cob2 -> Bool
(Ob Cob2 -> Ob Cob2 -> Bool)
-> (Ob Cob2 -> Ob Cob2 -> Bool) -> Eq (Ob Cob2)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Ob Cob2 -> Ob Cob2 -> Bool
$c/= :: Ob Cob2 -> Ob Cob2 -> Bool
== :: Ob Cob2 -> Ob Cob2 -> Bool
$c== :: Ob Cob2 -> Ob Cob2 -> Bool
Eq,Eq (Ob Cob2)
Eq (Ob Cob2) =>
(Ob Cob2 -> Ob Cob2 -> Ordering)
-> (Ob Cob2 -> Ob Cob2 -> Bool)
-> (Ob Cob2 -> Ob Cob2 -> Bool)
-> (Ob Cob2 -> Ob Cob2 -> Bool)
-> (Ob Cob2 -> Ob Cob2 -> Bool)
-> (Ob Cob2 -> Ob Cob2 -> Ob Cob2)
-> (Ob Cob2 -> Ob Cob2 -> Ob Cob2)
-> Ord (Ob Cob2)
Ob Cob2 -> Ob Cob2 -> Bool
Ob Cob2 -> Ob Cob2 -> Ordering
Ob Cob2 -> Ob Cob2 -> Ob Cob2
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Ob Cob2 -> Ob Cob2 -> Ob Cob2
$cmin :: Ob Cob2 -> Ob Cob2 -> Ob Cob2
max :: Ob Cob2 -> Ob Cob2 -> Ob Cob2
$cmax :: Ob Cob2 -> Ob Cob2 -> Ob Cob2
>= :: Ob Cob2 -> Ob Cob2 -> Bool
$c>= :: Ob Cob2 -> Ob Cob2 -> Bool
> :: Ob Cob2 -> Ob Cob2 -> Bool
$c> :: Ob Cob2 -> Ob Cob2 -> Bool
<= :: Ob Cob2 -> Ob Cob2 -> Bool
$c<= :: Ob Cob2 -> Ob Cob2 -> Bool
< :: Ob Cob2 -> Ob Cob2 -> Bool
$c< :: Ob Cob2 -> Ob Cob2 -> Bool
compare :: Ob Cob2 -> Ob Cob2 -> Ordering
$ccompare :: Ob Cob2 -> Ob Cob2 -> Ordering
$cp1Ord :: Eq (Ob Cob2)
Ord,Int -> Ob Cob2 -> ShowS
[Ob Cob2] -> ShowS
Ob Cob2 -> String
(Int -> Ob Cob2 -> ShowS)
-> (Ob Cob2 -> String) -> ([Ob Cob2] -> ShowS) -> Show (Ob Cob2)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Ob Cob2] -> ShowS
$cshowList :: [Ob Cob2] -> ShowS
show :: Ob Cob2 -> String
$cshow :: Ob Cob2 -> String
showsPrec :: Int -> Ob Cob2 -> ShowS
$cshowsPrec :: Int -> Ob Cob2 -> ShowS
Show)
    data Ar Cob2 = Id Int
                 | Unit
                 | Mult
                 | Counit
                 | Comult
                 | Par (Ar Cob2) (Ar Cob2)
                 | Seq (Ar Cob2) (Ar Cob2)
                 deriving (Ar Cob2 -> Ar Cob2 -> Bool
(Ar Cob2 -> Ar Cob2 -> Bool)
-> (Ar Cob2 -> Ar Cob2 -> Bool) -> Eq (Ar Cob2)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Ar Cob2 -> Ar Cob2 -> Bool
$c/= :: Ar Cob2 -> Ar Cob2 -> Bool
== :: Ar Cob2 -> Ar Cob2 -> Bool
$c== :: Ar Cob2 -> Ar Cob2 -> Bool
Eq,Eq (Ar Cob2)
Eq (Ar Cob2) =>
(Ar Cob2 -> Ar Cob2 -> Ordering)
-> (Ar Cob2 -> Ar Cob2 -> Bool)
-> (Ar Cob2 -> Ar Cob2 -> Bool)
-> (Ar Cob2 -> Ar Cob2 -> Bool)
-> (Ar Cob2 -> Ar Cob2 -> Bool)
-> (Ar Cob2 -> Ar Cob2 -> Ar Cob2)
-> (Ar Cob2 -> Ar Cob2 -> Ar Cob2)
-> Ord (Ar Cob2)
Ar Cob2 -> Ar Cob2 -> Bool
Ar Cob2 -> Ar Cob2 -> Ordering
Ar Cob2 -> Ar Cob2 -> Ar Cob2
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Ar Cob2 -> Ar Cob2 -> Ar Cob2
$cmin :: Ar Cob2 -> Ar Cob2 -> Ar Cob2
max :: Ar Cob2 -> Ar Cob2 -> Ar Cob2
$cmax :: Ar Cob2 -> Ar Cob2 -> Ar Cob2
>= :: Ar Cob2 -> Ar Cob2 -> Bool
$c>= :: Ar Cob2 -> Ar Cob2 -> Bool
> :: Ar Cob2 -> Ar Cob2 -> Bool
$c> :: Ar Cob2 -> Ar Cob2 -> Bool
<= :: Ar Cob2 -> Ar Cob2 -> Bool
$c<= :: Ar Cob2 -> Ar Cob2 -> Bool
< :: Ar Cob2 -> Ar Cob2 -> Bool
$c< :: Ar Cob2 -> Ar Cob2 -> Bool
compare :: Ar Cob2 -> Ar Cob2 -> Ordering
$ccompare :: Ar Cob2 -> Ar Cob2 -> Ordering
$cp1Ord :: Eq (Ar Cob2)
Ord,Int -> Ar Cob2 -> ShowS
[Ar Cob2] -> ShowS
Ar Cob2 -> String
(Int -> Ar Cob2 -> ShowS)
-> (Ar Cob2 -> String) -> ([Ar Cob2] -> ShowS) -> Show (Ar Cob2)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Ar Cob2] -> ShowS
$cshowList :: [Ar Cob2] -> ShowS
show :: Ar Cob2 -> String
$cshow :: Ar Cob2 -> String
showsPrec :: Int -> Ar Cob2 -> ShowS
$cshowsPrec :: Int -> Ar Cob2 -> ShowS
Show)
    id_ :: Ob Cob2 -> Ar Cob2
id_ (O n) = Int -> Ar Cob2
Id Int
n
    source :: Ar Cob2 -> Ob Cob2
source (Id n) = Int -> Ob Cob2
O Int
n
    source Unit = Int -> Ob Cob2
O 0
    source Mult = Int -> Ob Cob2
O 2
    source Counit = Int -> Ob Cob2
O 1
    source Comult = Int -> Ob Cob2
O 1
    source (Par a b) = Int -> Ob Cob2
O (Int
sa Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
sb) where O sa = Ar Cob2 -> Ob Cob2
forall c. MCategory c => Ar c -> Ob c
source Ar Cob2
a; O sb = Ar Cob2 -> Ob Cob2
forall c. MCategory c => Ar c -> Ob c
source Ar Cob2
b
    source (Seq a b) = Ar Cob2 -> Ob Cob2
forall c. MCategory c => Ar c -> Ob c
source Ar Cob2
a
    target :: Ar Cob2 -> Ob Cob2
target (Id n) = Int -> Ob Cob2
O Int
n
    target Unit = Int -> Ob Cob2
O 1
    target Mult = Int -> Ob Cob2
O 1
    target Counit = Int -> Ob Cob2
O 0
    target Comult = Int -> Ob Cob2
O 2
    target (Par a b) = Int -> Ob Cob2
O (Int
ta Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
tb) where O ta = Ar Cob2 -> Ob Cob2
forall c. MCategory c => Ar c -> Ob c
target Ar Cob2
a; O tb = Ar Cob2 -> Ob Cob2
forall c. MCategory c => Ar c -> Ob c
target Ar Cob2
b
    target (Seq a b) = Ar Cob2 -> Ob Cob2
forall c. MCategory c => Ar c -> Ob c
target Ar Cob2
b
    a :: Ar Cob2
a >>> :: Ar Cob2 -> Ar Cob2 -> Ar Cob2
>>> b :: Ar Cob2
b | Ar Cob2 -> Ob Cob2
forall c. MCategory c => Ar c -> Ob c
target Ar Cob2
a Ob Cob2 -> Ob Cob2 -> Bool
forall a. Eq a => a -> a -> Bool
== Ar Cob2 -> Ob Cob2
forall c. MCategory c => Ar c -> Ob c
source Ar Cob2
b = Ar Cob2 -> Ar Cob2 -> Ar Cob2
Seq Ar Cob2
a Ar Cob2
b

instance Monoidal Cob2 where
    tunit :: Ob Cob2
tunit = Int -> Ob Cob2
O 0
    tob :: Ob Cob2 -> Ob Cob2 -> Ob Cob2
tob (O a) (O b) = Int -> Ob Cob2
O (Int
aInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
b)
    tar :: Ar Cob2 -> Ar Cob2 -> Ar Cob2
tar a :: Ar Cob2
a b :: Ar Cob2
b = Ar Cob2 -> Ar Cob2 -> Ar Cob2
Par Ar Cob2
a Ar Cob2
b

-- rewrite a Cob2 so that it is a Seq of Pars
-- (this isn't necessarily going to help us towards a normal form - there may not even be one
rewrite :: Ar Cob2 -> Ar Cob2
rewrite (Par (Seq a1 a2) (Seq b1 b2)) =
    Ar Cob2 -> Ar Cob2 -> Ar Cob2
Seq (Ar Cob2 -> Ar Cob2 -> Ar Cob2
Par Ar Cob2
idSourceA Ar Cob2
b1')
        ( (Ar Cob2 -> Ar Cob2 -> Ar Cob2
Seq (Ar Cob2 -> Ar Cob2 -> Ar Cob2
Par Ar Cob2
idSourceA Ar Cob2
b2')
               (Ar Cob2 -> Ar Cob2 -> Ar Cob2
Seq (Ar Cob2 -> Ar Cob2 -> Ar Cob2
Par Ar Cob2
a1' Ar Cob2
idTargetB)
                    (Ar Cob2 -> Ar Cob2 -> Ar Cob2
Par Ar Cob2
a2' Ar Cob2
idTargetB) ) ) )
    where idSourceA :: Ar Cob2
idSourceA = Ob Cob2 -> Ar Cob2
forall c. MCategory c => Ob c -> Ar c
id_ (Ar Cob2 -> Ob Cob2
forall c. MCategory c => Ar c -> Ob c
source Ar Cob2
a1)
          idTargetB :: Ar Cob2
idTargetB = Ob Cob2 -> Ar Cob2
forall c. MCategory c => Ob c -> Ar c
id_ (Ar Cob2 -> Ob Cob2
forall c. MCategory c => Ar c -> Ob c
target Ar Cob2
b2)
          a1' :: Ar Cob2
a1' = Ar Cob2 -> Ar Cob2
rewrite Ar Cob2
a1
          a2' :: Ar Cob2
a2' = Ar Cob2 -> Ar Cob2
rewrite Ar Cob2
a2
          b1' :: Ar Cob2
b1' = Ar Cob2 -> Ar Cob2
rewrite Ar Cob2
b1
          b2' :: Ar Cob2
b2' = Ar Cob2 -> Ar Cob2
rewrite Ar Cob2
b2
rewrite x :: Ar Cob2
x = Ar Cob2
x