    -- 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