{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# OPTIONS_GHC -Wno-incomplete-patterns -Wno-overlapping-patterns #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Control.Category.FreeSMC where

import Prelude hiding ((.),id,curry)
import Control.Category.Constrained
import Data.Monoid
import Data.Kind
import Data.Type.Equality

newtype Sho a b = Sho {forall {k} {k} (a :: k) (b :: k). Sho a b -> Int -> ShowS
fromSho :: Int -> ShowS}

instance Show (Sho a b) where
  showsPrec :: Int -> Sho a b -> ShowS
showsPrec Int
d (Sho Int -> ShowS
f) = Int -> ShowS
f Int
d

shoCon :: String -> Sho a b
shoCon :: forall {k} {k} (a :: k) (b :: k). [Char] -> Sho a b
shoCon [Char]
name = forall {k} {k} (a :: k) (b :: k). (Int -> ShowS) -> Sho a b
Sho forall a b. (a -> b) -> a -> b
$ \Int
_ -> [Char] -> ShowS
showString [Char]
name

instance Category Sho where
  type Obj Sho = Trivial
  id :: forall a. Obj Sho a => Sho a a
id = forall {k} {k} (a :: k) (b :: k). [Char] -> Sho a b
shoCon [Char]
"id"
  Sho Int -> ShowS
f ∘ :: forall a b c.
(Obj Sho a, Obj Sho b, Obj Sho c) =>
Sho b c -> Sho a b -> Sho a c
∘ Sho Int -> ShowS
g = forall {k} {k} (a :: k) (b :: k). (Int -> ShowS) -> Sho a b
Sho forall a b. (a -> b) -> a -> b
$ \Int
d -> Bool -> ShowS -> ShowS
showParen (Int
d forall a. Eq a => a -> a -> Bool
/= Int
0) (Int -> ShowS
f Int
0 forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. [Char] -> ShowS
showString [Char]
" ∘ " forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. Int -> ShowS
g Int
0)

instance Monoidal Sho where
  swap :: forall a b. (Obj Sho a, Obj Sho b) => Sho (a ⊗ b) (b ⊗ a)
swap = forall {k} {k} (a :: k) (b :: k). [Char] -> Sho a b
shoCon [Char]
"swap"
  assoc :: forall a b c.
(Obj Sho a, Obj Sho b, Obj Sho c) =>
Sho ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
assoc = forall {k} {k} (a :: k) (b :: k). [Char] -> Sho a b
shoCon [Char]
"assoc"
  assoc' :: forall a b c.
(Obj Sho a, Obj Sho b, Obj Sho c) =>
Sho (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
assoc' = forall {k} {k} (a :: k) (b :: k). [Char] -> Sho a b
shoCon [Char]
"assoc'"
  unitor :: forall a. Obj Sho a => Sho a (a ⊗ ())
unitor = forall {k} {k} (a :: k) (b :: k). [Char] -> Sho a b
shoCon [Char]
"unitor"
  unitor' :: forall a. Obj Sho a => Sho (a ⊗ ()) a
unitor' = forall {k} {k} (a :: k) (b :: k). [Char] -> Sho a b
shoCon [Char]
"unitor'"
  Sho Int -> ShowS
f × :: forall a b c d.
(Obj Sho a, Obj Sho b, Obj Sho c, Obj Sho d) =>
Sho a b -> Sho c d -> Sho (a ⊗ c) (b ⊗ d)
× Sho Int -> ShowS
g = forall {k} {k} (a :: k) (b :: k). (Int -> ShowS) -> Sho a b
Sho forall a b. (a -> b) -> a -> b
$ \Int
d -> Bool -> ShowS -> ShowS
showParen (Int
d forall a. Eq a => a -> a -> Bool
/= Int
0) (Int -> ShowS
f Int
2 forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. [Char] -> ShowS
showString [Char]
" × " forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. Int -> ShowS
g Int
2)

instance Cartesian Sho where
  dis :: forall a. Obj Sho a => Sho a ()
dis = forall {k} {k} (a :: k) (b :: k). [Char] -> Sho a b
shoCon [Char]
"dis"
  dup :: forall a. (Obj Sho a, Obj Sho (a ⊗ a)) => Sho a (a ⊗ a)
dup = forall {k} {k} (a :: k) (b :: k). [Char] -> Sho a b
shoCon [Char]
"dup"
  exl :: forall a b. O2 Sho a b => Sho (a ⊗ b) a
exl = forall {k} {k} (a :: k) (b :: k). [Char] -> Sho a b
shoCon [Char]
"exl"
  exr :: forall a b. O2 Sho a b => Sho (a ⊗ b) b
exr = forall {k} {k} (a :: k) (b :: k). [Char] -> Sho a b
shoCon [Char]
"exr"
  Sho Int -> ShowS
f ▵ :: forall a b c.
(Obj Sho a, Obj Sho b, Obj Sho c) =>
Sho a b -> Sho a c -> Sho a (b ⊗ c)
▵ Sho Int -> ShowS
g = forall {k} {k} (a :: k) (b :: k). (Int -> ShowS) -> Sho a b
Sho forall a b. (a -> b) -> a -> b
$ \Int
d -> Bool -> ShowS -> ShowS
showParen (Int
d forall a. Eq a => a -> a -> Bool
/= Int
0) (Int -> ShowS
f Int
2 forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. [Char] -> ShowS
showString [Char]
" ▵ " forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. Int -> ShowS
g Int
2)

class HasShow k where
  toShow :: k a b -> Sho a b

instance HasShow Sho where
  toShow :: forall (a :: k) (b :: k). Sho a b -> Sho a b
toShow = forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id


instance (forall x y. (con x, con y) => Show (k x y)) => Show  (Cat k con a b) where
  show :: Cat k con a b -> [Char]
show Cat k con a b
x = forall a. Show a => Int -> a -> ShowS
showsPrec (-Int
1) Cat k con a b
x [Char]
""
  showsPrec :: Int -> Cat k con a b -> ShowS
showsPrec Int
d = \case
    Cat k con a b
I -> [Char] -> ShowS
showString [Char]
"id"
    Cat k con a b
S -> [Char] -> ShowS
showString [Char]
"swap"
    Cat k con a b
A  -> [Char] -> ShowS
showString [Char]
"assoc"
    Cat k con a b
A' -> [Char] -> ShowS
showString [Char]
"assoc'"
    U Unitor con a b
a -> {-showString "[" .-} forall {k} {k} (a :: k) (b :: k). Sho a b -> Int -> ShowS
fromSho (forall (k :: * -> * -> *) a b (con :: * -> Constraint).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Monoidal k, Obj k a, Obj k b) =>
Unitor (Obj k) a b -> k a b
evalUnitor (forall (con :: * -> Constraint) a b.
Unitor con a b -> Unitor Trivial a b
trivializeUnitor Unitor con a b
a)) Int
0 {-. showString "]"-}
    U' Unitor con b a
a -> {-showString "[" .-} forall {k} {k} (a :: k) (b :: k). Sho a b -> Int -> ShowS
fromSho (forall (k :: * -> * -> *) a b (con :: * -> Constraint).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Monoidal k, Obj k a, Obj k b) =>
Unitor (Obj k) b a -> k a b
evalUnitor' (forall (con :: * -> Constraint) a b.
Unitor con a b -> Unitor Trivial a b
trivializeUnitor Unitor con b a
a)) Int
0 {-. showString "]"-}
    X k a b
s -> [Char] -> ShowS
showString (forall a. Show a => a -> [Char]
show k a b
s)
    Cat k con b b
f :.: Cat k con a b
g -> Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
>  Int
0) (forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 Cat k con b b
f forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. [Char] -> ShowS
showString [Char]
" ∘ " forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 Cat k con a b
g)
    Cat k con a b
f :×: Cat k con c d
g -> Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> -Int
1) (forall a. Show a => Int -> a -> ShowS
showsPrec Int
2 Cat k con a b
f forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. [Char] -> ShowS
showString [Char]
" × " forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
2 Cat k con c d
g)


showDbg :: Int -> Cat k con a b -> ShowS
showDbg :: forall (k :: * -> * -> *) (con :: * -> Constraint) a b.
Int -> Cat k con a b -> ShowS
showDbg Int
d = \case
    X k a b
_ -> [Char] -> ShowS
showString [Char]
"?"

    Cat k con a b
I -> [Char] -> ShowS
showString [Char]
"id"
    Cat k con b b
f :.: Cat k con a b
g -> Bool -> ShowS -> ShowS
showParen (Int
d forall a. Eq a => a -> a -> Bool
/= Int
0) (forall (k :: * -> * -> *) (con :: * -> Constraint) a b.
Int -> Cat k con a b -> ShowS
showDbg Int
0 Cat k con b b
f forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. [Char] -> ShowS
showString [Char]
" ∘ " forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *) (con :: * -> Constraint) a b.
Int -> Cat k con a b -> ShowS
showDbg Int
0 Cat k con a b
g)

    Cat k con a b
f :×: Cat k con c d
g -> Bool -> ShowS -> ShowS
showParen Bool
True (forall (k :: * -> * -> *) (con :: * -> Constraint) a b.
Int -> Cat k con a b -> ShowS
showDbg Int
2 Cat k con a b
f forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. [Char] -> ShowS
showString [Char]
" × " forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *) (con :: * -> Constraint) a b.
Int -> Cat k con a b -> ShowS
showDbg Int
2 Cat k con c d
g)
    Cat k con a b
S -> [Char] -> ShowS
showString [Char]
"σ"
    Cat k con a b
A  -> [Char] -> ShowS
showString [Char]
"α"
    Cat k con a b
A' -> [Char] -> ShowS
showString [Char]
"α'"
    U Unitor con a b
_ -> [Char] -> ShowS
showString [Char]
"ρ"
    U' Unitor con b a
a  -> [Char] -> ShowS
showString ([Char]
"ρ'(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Unitor con b a
a forall a. [a] -> [a] -> [a]
++ [Char]
")")



parens :: [Char] -> [Char]
parens :: ShowS
parens [Char]
x = [Char]
"("forall a. Semigroup a => a -> a -> a
<> [Char]
x forall a. Semigroup a => a -> a -> a
<>[Char]
")"

mapGenerators :: (con a, con b) => (forall x y. (con x, con y) => k x y -> k' x y) -> Cat k con a b -> Cat k' con a b
mapGenerators :: forall (con :: * -> Constraint) a b (k :: * -> * -> *)
       (k' :: * -> * -> *).
(con a, con b) =>
(forall x y. (con x, con y) => k x y -> k' x y)
-> Cat k con a b -> Cat k' con a b
mapGenerators forall x y. (con x, con y) => k x y -> k' x y
f = \case
  X k a b
g -> forall (k :: * -> * -> *) (con :: * -> Constraint) a b.
(con a, con b) =>
k a b -> Cat k con a b
X (forall x y. (con x, con y) => k x y -> k' x y
f k a b
g)

  Cat k con a b
I -> forall (k :: * -> * -> *) (con :: * -> Constraint) a. Cat k con a a
I
  Cat k con b b
a :.: Cat k con a b
b -> forall (con :: * -> Constraint) a b (k :: * -> * -> *)
       (k' :: * -> * -> *).
(con a, con b) =>
(forall x y. (con x, con y) => k x y -> k' x y)
-> Cat k con a b -> Cat k' con a b
mapGenerators forall x y. (con x, con y) => k x y -> k' x y
f Cat k con b b
a forall (con :: * -> Constraint) a (k :: * -> * -> *) c a.
con a =>
Cat k con a c -> Cat k con a a -> Cat k con a c
:.: forall (con :: * -> Constraint) a b (k :: * -> * -> *)
       (k' :: * -> * -> *).
(con a, con b) =>
(forall x y. (con x, con y) => k x y -> k' x y)
-> Cat k con a b -> Cat k' con a b
mapGenerators forall x y. (con x, con y) => k x y -> k' x y
f Cat k con a b
b

  Cat k con a b
a :×: Cat k con c d
b -> forall (con :: * -> Constraint) a b (k :: * -> * -> *)
       (k' :: * -> * -> *).
(con a, con b) =>
(forall x y. (con x, con y) => k x y -> k' x y)
-> Cat k con a b -> Cat k' con a b
mapGenerators forall x y. (con x, con y) => k x y -> k' x y
f Cat k con a b
a forall (con :: * -> Constraint) a b c d (k :: * -> * -> *).
(con a, con b, con c, con d) =>
Cat k con a b -> Cat k con c d -> Cat k con (a ⊗ c) (b ⊗ d)
:×: forall (con :: * -> Constraint) a b (k :: * -> * -> *)
       (k' :: * -> * -> *).
(con a, con b) =>
(forall x y. (con x, con y) => k x y -> k' x y)
-> Cat k con a b -> Cat k' con a b
mapGenerators forall x y. (con x, con y) => k x y -> k' x y
f Cat k con c d
b
  Cat k con a b
A -> forall (con :: * -> Constraint) a b c (k :: * -> * -> *).
(con a, con b, con c) =>
Cat k con ((a, b), c) (a, (b, c))
A
  Cat k con a b
A' -> forall (con :: * -> Constraint) a b c (k :: * -> * -> *).
(con a, con b, con c) =>
Cat k con (a, (b, c)) ((a, b), c)
A'
  Cat k con a b
S -> forall (con :: * -> Constraint) a b (k :: * -> * -> *).
(con a, con b) =>
Cat k con (a, b) (b, a)
S
  U Unitor con a b
x -> forall (con :: * -> Constraint) a b (k :: * -> * -> *).
Unitor con a b -> Cat k con a b
U Unitor con a b
x
  U' Unitor con b a
x -> forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con b a
x

  Cat k con a b
x -> forall a. HasCallStack => [Char] -> a
error (forall (k :: * -> * -> *) (con :: * -> Constraint) a b.
Int -> Cat k con a b -> ShowS
showDbg Int
0 Cat k con a b
x [Char]
" (Free.mapGenerators)")


instance Show (Unitor con a b) where
  show :: Unitor con a b -> [Char]
show Unitor con a b
UL = [Char]
"⟨"
  show Unitor con a b
UR = [Char]
"⟩"
  show (IL Unitor con a b
a) = [Char]
"⟨" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Unitor con a b
a
  show (IR Unitor con a b
a) = [Char]
"⟩" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Unitor con a b
a
data Unitor con a b where
  UL :: Unitor con a ((),a)
  UR :: Unitor con a (a,())
  IL :: (con a, con b, con c) => Unitor con a b -> Unitor con (a,c) (b,c)
  IR :: (con a, con b, con c) => Unitor con a b -> Unitor con (c,a) (c,b)

compareUnitors :: Unitor con a b -> Unitor con a b' -> Maybe (b :~: b')
compareUnitors :: forall (con :: * -> Constraint) a b b'.
Unitor con a b -> Unitor con a b' -> Maybe (b :~: b')
compareUnitors Unitor con a b
UL Unitor con a b'
UL = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
compareUnitors Unitor con a b
UR Unitor con a b'
UR = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
compareUnitors (IL Unitor con a b
a) (IL Unitor con a b
b) = case forall (con :: * -> Constraint) a b b'.
Unitor con a b -> Unitor con a b' -> Maybe (b :~: b')
compareUnitors Unitor con a b
a Unitor con a b
b of Maybe (b :~: b)
Nothing -> forall a. Maybe a
Nothing; Just b :~: b
Refl -> forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
compareUnitors (IR Unitor con a b
a) (IR Unitor con a b
b) = case forall (con :: * -> Constraint) a b b'.
Unitor con a b -> Unitor con a b' -> Maybe (b :~: b')
compareUnitors Unitor con a b
a Unitor con a b
b of Maybe (b :~: b)
Nothing -> forall a. Maybe a
Nothing; Just b :~: b
Refl -> forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
compareUnitors Unitor con a b
_ Unitor con a b'
_ = forall a. Maybe a
Nothing

trivializeUnitor :: Unitor con a b -> Unitor Trivial a b
trivializeUnitor :: forall (con :: * -> Constraint) a b.
Unitor con a b -> Unitor Trivial a b
trivializeUnitor Unitor con a b
UL = forall (con :: * -> Constraint) a. Unitor con a ((), a)
UL
trivializeUnitor Unitor con a b
UR = forall (con :: * -> Constraint) a. Unitor con a (a, ())
UR
trivializeUnitor (IL Unitor con a b
f) = forall (con :: * -> Constraint) a b c.
(con a, con b, con c) =>
Unitor con a b -> Unitor con (a ⊗ c) (b, c)
IL (forall (con :: * -> Constraint) a b.
Unitor con a b -> Unitor Trivial a b
trivializeUnitor Unitor con a b
f)
trivializeUnitor (IR Unitor con a b
f) = forall (con :: * -> Constraint) a b c.
(con a, con b, con c) =>
Unitor con a b -> Unitor con (c, a) (c, b)
IR (forall (con :: * -> Constraint) a b.
Unitor con a b -> Unitor Trivial a b
trivializeUnitor Unitor con a b
f)

commuteUnitors :: (ProdObj con, forall α β. (con α, con β) => con (α,β), con (),
                  con a, con b) => Unitor con c b -> Unitor con a b -> Cat cat con a c
commuteUnitors :: forall (con :: * -> Constraint) a b c (cat :: * -> * -> *).
(ProdObj con, forall α β. (con α, con β) => con (α, β), con (),
 con a, con b) =>
Unitor con c b -> Unitor con a b -> Cat cat con a c
commuteUnitors Unitor con c b
UL Unitor con a b
UL = forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id
commuteUnitors Unitor con c b
UL Unitor con a b
UR = forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id
commuteUnitors Unitor con c b
UR Unitor con a b
UR = forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id
commuteUnitors Unitor con c b
UR Unitor con a b
UL = forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id
commuteUnitors (IL Unitor con a b
a) (IL Unitor con a b
b) = forall (con :: * -> Constraint) a b c (cat :: * -> * -> *).
(ProdObj con, forall α β. (con α, con β) => con (α, β), con (),
 con a, con b) =>
Unitor con c b -> Unitor con a b -> Cat cat con a c
commuteUnitors Unitor con a b
a Unitor con a b
b forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id
commuteUnitors (IR Unitor con a b
a) (IR Unitor con a b
b) = forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (con :: * -> Constraint) a b c (cat :: * -> * -> *).
(ProdObj con, forall α β. (con α, con β) => con (α, β), con (),
 con a, con b) =>
Unitor con c b -> Unitor con a b -> Cat cat con a c
commuteUnitors Unitor con a b
a Unitor con a b
b
commuteUnitors (IR Unitor con a b
a) (IL Unitor con a b
b) = forall (con :: * -> Constraint) a b (k :: * -> * -> *).
Unitor con a b -> Cat k con a b
U (forall (con :: * -> Constraint) a b c.
(con a, con b, con c) =>
Unitor con a b -> Unitor con (a ⊗ c) (b, c)
IL Unitor con a b
b) forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
.  forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' (forall (con :: * -> Constraint) a b c.
(con a, con b, con c) =>
Unitor con a b -> Unitor con (c, a) (c, b)
IR Unitor con a b
a)
commuteUnitors (IL Unitor con a b
a) (IR Unitor con a b
b) = forall (con :: * -> Constraint) a b (k :: * -> * -> *).
Unitor con a b -> Cat k con a b
U (forall (con :: * -> Constraint) a b c.
(con a, con b, con c) =>
Unitor con a b -> Unitor con (c, a) (c, b)
IR Unitor con a b
b) forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
.  forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' (forall (con :: * -> Constraint) a b c.
(con a, con b, con c) =>
Unitor con a b -> Unitor con (a ⊗ c) (b, c)
IL Unitor con a b
a)
commuteUnitors Unitor con c b
UL (IR Unitor con a b
a) = forall (con :: * -> Constraint) a b (k :: * -> * -> *).
Unitor con a b -> Cat k con a b
U Unitor con a b
a forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' forall (con :: * -> Constraint) a. Unitor con a ((), a)
UL
commuteUnitors Unitor con c b
UR (IL Unitor con a b
a) = forall (con :: * -> Constraint) a b (k :: * -> * -> *).
Unitor con a b -> Cat k con a b
U Unitor con a b
a forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' forall (con :: * -> Constraint) a. Unitor con a (a, ())
UR
commuteUnitors (IR Unitor con a b
a) Unitor con a b
UL = forall (con :: * -> Constraint) a b (k :: * -> * -> *).
Unitor con a b -> Cat k con a b
U forall (con :: * -> Constraint) a. Unitor con a ((), a)
UL forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con a b
a
commuteUnitors (IL Unitor con a b
a) Unitor con a b
UR = forall (con :: * -> Constraint) a b (k :: * -> * -> *).
Unitor con a b -> Cat k con a b
U forall (con :: * -> Constraint) a. Unitor con a (a, ())
UR forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con a b
a


data Cat k (con :: Type -> Constraint) a b where
  A :: (con a, con b, con c) => Cat k con ((a,b),c) (a,(b,c))
  A' :: (con a, con b, con c) => Cat k con (a,(b,c)) ((a,b),c)
  S ::  (con a, con b) => Cat k con (a,b) (b,a) 
  Embed :: (con a, con b) => k a b -> Cat k con a b
  I :: Cat k con a a
  U :: Unitor con a b -> Cat k con a b
  U' :: Unitor con b a -> Cat k con a b

  (:.:) :: con b => (Cat k con b c) -> (Cat k con a b) -> (Cat k con a c)
  (:×:) :: (con a, con b, con c, con d) => (Cat k con a b) -> (Cat k con c d) -> (Cat k con (a ⊗ c) (b ⊗ d))


instance Invertible (Cat k con) where
  dual :: Cat k con a b -> Cat k con b a
  dual :: forall a b. Cat k con a b -> Cat k con b a
dual = \case
    Cat k con a b
I -> forall (k :: * -> * -> *) (con :: * -> Constraint) a. Cat k con a a
I
    Cat k con a b
f :×: Cat k con c d
g -> forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Invertible k =>
k a b -> k b a
dual Cat k con a b
f forall (con :: * -> Constraint) a b c d (k :: * -> * -> *).
(con a, con b, con c, con d) =>
Cat k con a b -> Cat k con c d -> Cat k con (a ⊗ c) (b ⊗ d)
:×: forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Invertible k =>
k a b -> k b a
dual Cat k con c d
g
    Cat k con b b
f :.: Cat k con a b
g -> forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Invertible k =>
k a b -> k b a
dual Cat k con a b
g forall (con :: * -> Constraint) a (k :: * -> * -> *) c a.
con a =>
Cat k con a c -> Cat k con a a -> Cat k con a c
:.: forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Invertible k =>
k a b -> k b a
dual Cat k con b b
f
    Cat k con a b
S -> forall (con :: * -> Constraint) a b (k :: * -> * -> *).
(con a, con b) =>
Cat k con (a, b) (b, a)
S
    Cat k con a b
A -> forall (con :: * -> Constraint) a b c (k :: * -> * -> *).
(con a, con b, con c) =>
Cat k con (a, (b, c)) ((a, b), c)
A'
    Cat k con a b
A' -> forall (con :: * -> Constraint) a b c (k :: * -> * -> *).
(con a, con b, con c) =>
Cat k con ((a, b), c) (a, (b, c))
A

assocRight :: Cat k obj x y -> Cat k obj x y
assocRight :: forall (k :: * -> * -> *) (obj :: * -> Constraint) x y.
Cat k obj x y -> Cat k obj x y
assocRight (Cat k obj b y
a :.: (forall (k :: * -> * -> *) (obj :: * -> Constraint) x y.
Cat k obj x y -> Cat k obj x y
assocRight -> (Cat k obj b b
b :.: Cat k obj x b
c))) = (Cat k obj b y
a forall (con :: * -> Constraint) a (k :: * -> * -> *) c a.
con a =>
Cat k con a c -> Cat k con a a -> Cat k con a c
:.: Cat k obj b b
b) forall (con :: * -> Constraint) a (k :: * -> * -> *) c a.
con a =>
Cat k con a c -> Cat k con a a -> Cat k con a c
:.: Cat k obj x b
c
assocRight Cat k obj x y
x = Cat k obj x y
x

rightView :: (obj a, obj c) => Cat k obj a c -> Cat k obj a c
rightView :: forall (obj :: * -> Constraint) a c (k :: * -> * -> *).
(obj a, obj c) =>
Cat k obj a c -> Cat k obj a c
rightView (forall (k :: * -> * -> *) (obj :: * -> Constraint) x y.
Cat k obj x y -> Cat k obj x y
assocRight -> (Cat k obj b c
a :.: Cat k obj a b
b)) = Cat k obj b c
a forall (con :: * -> Constraint) a (k :: * -> * -> *) c a.
con a =>
Cat k con a c -> Cat k con a a -> Cat k con a c
:.: Cat k obj a b
b
rightView Cat k obj a c
x = forall (k :: * -> * -> *) (con :: * -> Constraint) a. Cat k con a a
I forall (con :: * -> Constraint) a (k :: * -> * -> *) c a.
con a =>
Cat k con a c -> Cat k con a a -> Cat k con a c
:.: Cat k obj a c
x

assocLeft :: Cat k obj x y -> Cat k obj x y
assocLeft :: forall (k :: * -> * -> *) (obj :: * -> Constraint) x y.
Cat k obj x y -> Cat k obj x y
assocLeft ((forall (k :: * -> * -> *) (obj :: * -> Constraint) x y.
Cat k obj x y -> Cat k obj x y
assocLeft -> (Cat k obj b y
a :.: Cat k obj b b
b)) :.: Cat k obj x b
c) = Cat k obj b y
a forall (con :: * -> Constraint) a (k :: * -> * -> *) c a.
con a =>
Cat k con a c -> Cat k con a a -> Cat k con a c
:.: (Cat k obj b b
b forall (con :: * -> Constraint) a (k :: * -> * -> *) c a.
con a =>
Cat k con a c -> Cat k con a a -> Cat k con a c
:.: Cat k obj x b
c)
assocLeft Cat k obj x y
x = Cat k obj x y
x

leftView :: (obj a, obj c) => Cat k obj a c -> Cat k obj a c
leftView :: forall (obj :: * -> Constraint) a c (k :: * -> * -> *).
(obj a, obj c) =>
Cat k obj a c -> Cat k obj a c
leftView (forall (k :: * -> * -> *) (obj :: * -> Constraint) x y.
Cat k obj x y -> Cat k obj x y
assocLeft -> (Cat k obj b c
a :.: Cat k obj a b
b)) = Cat k obj b c
a forall (con :: * -> Constraint) a (k :: * -> * -> *) c a.
con a =>
Cat k con a c -> Cat k con a a -> Cat k con a c
:.: Cat k obj a b
b
leftView Cat k obj a c
x = Cat k obj a c
x forall (con :: * -> Constraint) a (k :: * -> * -> *) c a.
con a =>
Cat k con a c -> Cat k con a a -> Cat k con a c
:.: forall (k :: * -> * -> *) (con :: * -> Constraint) a. Cat k con a a
I

pattern (:>:) ::  (obj x, obj y) => (obj b)  =>  Cat k obj b y -> Cat k obj x b -> Cat k obj x y
pattern f $b:>: :: forall (obj :: * -> Constraint) x y (k :: * -> * -> *) b.
(obj x, obj y, obj b) =>
Cat k obj b y -> Cat k obj x b -> Cat k obj x y
$m:>: :: forall {r} {obj :: * -> Constraint} {x} {y} {k :: * -> * -> *}.
(obj x, obj y) =>
Cat k obj x y
-> (forall {b}. obj b => Cat k obj b y -> Cat k obj x b -> r)
-> ((# #) -> r)
-> r
:>: g <- (rightView -> f :.: g)
  where Cat k obj b y
f :>: Cat k obj x b
g = Cat k obj b y
f forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. Cat k obj x b
g

pattern (:<:) ::  (obj x, obj y) => (obj b) => Cat k obj b y -> Cat k obj x b -> Cat k obj x y
pattern f $b:<: :: forall (obj :: * -> Constraint) x y (k :: * -> * -> *) b.
(obj x, obj y, obj b) =>
Cat k obj b y -> Cat k obj x b -> Cat k obj x y
$m:<: :: forall {r} {obj :: * -> Constraint} {x} {y} {k :: * -> * -> *}.
(obj x, obj y) =>
Cat k obj x y
-> (forall {b}. obj b => Cat k obj b y -> Cat k obj x b -> r)
-> ((# #) -> r)
-> r
:<: g <- (leftView -> f :.: g)
  where Cat k obj b y
f :<: Cat k obj x b
g = Cat k obj b y
f forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. Cat k obj x b
g

-- pattern Uncurry :: (obj a1, obj a2, obj c, obj (a1×a2)) => Cat k obj a1  (a2 -> c) -> Cat k obj (a1 × a2)  c
-- pattern Uncurry f <- Apply :<: (f :×: I)



evalM :: forall k a b con.
              (ProdObj con, forall x y. (con x, con y) => con (x,y), con (),
               con ~ Obj k, Monoidal k, Obj k a, Obj k b) => Cat k (Obj k) a b -> k a b
evalM :: forall (k :: * -> * -> *) a b (con :: * -> Constraint).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Monoidal k, Obj k a, Obj k b) =>
Cat k (Obj k) a b -> k a b
evalM Cat k (Obj k) a b
I          = forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id
evalM (Cat k (Obj k) a b
f :×: Cat k (Obj k) c d
g)  = forall (k :: * -> * -> *) a b (con :: * -> Constraint).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Monoidal k, Obj k a, Obj k b) =>
Cat k (Obj k) a b -> k a b
evalM Cat k (Obj k) a b
f forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (k :: * -> * -> *) a b (con :: * -> Constraint).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Monoidal k, Obj k a, Obj k b) =>
Cat k (Obj k) a b -> k a b
evalM Cat k (Obj k) c d
g
evalM (Cat k (Obj k) b b
f :.: Cat k (Obj k) a b
g)  = forall (k :: * -> * -> *) a b (con :: * -> Constraint).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Monoidal k, Obj k a, Obj k b) =>
Cat k (Obj k) a b -> k a b
evalM Cat k (Obj k) b b
f forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *) a b (con :: * -> Constraint).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Monoidal k, Obj k a, Obj k b) =>
Cat k (Obj k) a b -> k a b
evalM Cat k (Obj k) a b
g
evalM Cat k (Obj k) a b
A          = forall (k :: * -> * -> *) a b c.
(Monoidal k, Obj k a, Obj k b, Obj k c) =>
k ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
assoc
evalM Cat k (Obj k) a b
A'         = forall (k :: * -> * -> *) a b c.
(Monoidal k, Obj k a, Obj k b, Obj k c) =>
k (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
assoc'
evalM Cat k (Obj k) a b
S          = forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap
evalM (U Unitor (Obj k) a b
u)      = forall (k :: * -> * -> *) a b (con :: * -> Constraint).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Monoidal k, Obj k a, Obj k b) =>
Unitor (Obj k) a b -> k a b
evalUnitor Unitor (Obj k) a b
u
evalM (U' Unitor (Obj k) b a
u)     = forall (k :: * -> * -> *) a b (con :: * -> Constraint).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Monoidal k, Obj k a, Obj k b) =>
Unitor (Obj k) b a -> k a b
evalUnitor' Unitor (Obj k) b a
u
evalM (Embed k a b
ϕ)  = k a b
ϕ

evalCartesian :: forall k a b con.
              (ProdObj con, forall x y. (con x, con y) => con (x,y), con (),
               con ~ Obj k, Cartesian k, Obj k a, Obj k b) => Cat k (Obj k) a b -> k a b
evalCartesian :: forall (k :: * -> * -> *) a b (con :: * -> Constraint).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Cartesian k, Obj k a, Obj k b) =>
Cat k (Obj k) a b -> k a b
evalCartesian = \case
  Cat k (Obj k) a b
I -> forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id
  (Cat k (Obj k) a b
f :×: Cat k (Obj k) c d
g) -> forall (k :: * -> * -> *) a b (con :: * -> Constraint).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Cartesian k, Obj k a, Obj k b) =>
Cat k (Obj k) a b -> k a b
evalCartesian Cat k (Obj k) a b
f forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (k :: * -> * -> *) a b (con :: * -> Constraint).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Cartesian k, Obj k a, Obj k b) =>
Cat k (Obj k) a b -> k a b
evalCartesian Cat k (Obj k) c d
g
  (Cat k (Obj k) b b
f :.: Cat k (Obj k) a b
g) -> forall (k :: * -> * -> *) a b (con :: * -> Constraint).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Cartesian k, Obj k a, Obj k b) =>
Cat k (Obj k) a b -> k a b
evalCartesian Cat k (Obj k) b b
f forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *) a b (con :: * -> Constraint).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Cartesian k, Obj k a, Obj k b) =>
Cat k (Obj k) a b -> k a b
evalCartesian Cat k (Obj k) a b
g
  (X k a b
ϕ) -> k a b
ϕ
  Cat k (Obj k) a b
A -> forall (k :: * -> * -> *) a b c.
(Monoidal k, Obj k a, Obj k b, Obj k c) =>
k ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
assoc
  Cat k (Obj k) a b
A' -> forall (k :: * -> * -> *) a b c.
(Monoidal k, Obj k a, Obj k b, Obj k c) =>
k (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
assoc'
  Cat k (Obj k) a b
S -> forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap
  (U Unitor (Obj k) a b
u) -> forall (k :: * -> * -> *) a b (con :: * -> Constraint).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Monoidal k, Obj k a, Obj k b) =>
Unitor (Obj k) a b -> k a b
evalUnitor Unitor (Obj k) a b
u
  (U' Unitor (Obj k) b a
u) -> forall (k :: * -> * -> *) a b (con :: * -> Constraint).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Monoidal k, Obj k a, Obj k b) =>
Unitor (Obj k) b a -> k a b
evalUnitor' Unitor (Obj k) b a
u


evalUnitor :: forall k a b con.
              (ProdObj con, forall x y. (con x, con y) => con (x,y), con (),
               con ~ Obj k, Monoidal k, Obj k a, Obj k b)
           => Unitor (Obj k) a b -> k a b
evalUnitor :: forall (k :: * -> * -> *) a b (con :: * -> Constraint).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Monoidal k, Obj k a, Obj k b) =>
Unitor (Obj k) a b -> k a b
evalUnitor Unitor (Obj k) a b
UR = forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k a (a ⊗ ())
unitor
evalUnitor Unitor (Obj k) a b
UL = forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k a (a ⊗ ())
unitor
evalUnitor (IL Unitor (Obj k) a b
x) = forall (k :: * -> * -> *) a b (con :: * -> Constraint).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Monoidal k, Obj k a, Obj k b) =>
Unitor (Obj k) a b -> k a b
evalUnitor Unitor (Obj k) a b
x forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id
evalUnitor (IR Unitor (Obj k) a b
x) = forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (k :: * -> * -> *) a b (con :: * -> Constraint).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Monoidal k, Obj k a, Obj k b) =>
Unitor (Obj k) a b -> k a b
evalUnitor Unitor (Obj k) a b
x

evalUnitor' :: forall k a b con.
              (ProdObj con, forall x y. (con x, con y) => con (x,y), con (),
               con ~ Obj k, Monoidal k, Obj k a, Obj k b)
           => Unitor (Obj k) b a -> k a b
evalUnitor' :: forall (k :: * -> * -> *) a b (con :: * -> Constraint).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Monoidal k, Obj k a, Obj k b) =>
Unitor (Obj k) b a -> k a b
evalUnitor' Unitor (Obj k) b a
UR = forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k (a ⊗ ()) a
unitor'
evalUnitor' Unitor (Obj k) b a
UL = forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k (a ⊗ ()) a
unitor' forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap
evalUnitor' (IL Unitor (Obj k) a b
x) = forall (k :: * -> * -> *) a b (con :: * -> Constraint).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Monoidal k, Obj k a, Obj k b) =>
Unitor (Obj k) b a -> k a b
evalUnitor' Unitor (Obj k) a b
x forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id
evalUnitor' (IR Unitor (Obj k) a b
x) = forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (k :: * -> * -> *) a b (con :: * -> Constraint).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Monoidal k, Obj k a, Obj k b) =>
Unitor (Obj k) b a -> k a b
evalUnitor' Unitor (Obj k) a b
x
-- eval Dup = dup
-- eval Apply = apply
-- eval (Curry f) = curry (eval f)
---------------------------
-- Cat k obj - instances


pattern X :: forall (k :: Type -> Type -> Type) (con :: Type -> Constraint) a b. () => (con a, con b) => k a b -> Cat k con a b
pattern $bX :: forall (k :: * -> * -> *) (con :: * -> Constraint) a b.
(con a, con b) =>
k a b -> Cat k con a b
$mX :: forall {r} {k :: * -> * -> *} {con :: * -> Constraint} {a} {b}.
Cat k con a b
-> ((con a, con b) => k a b -> r) -> ((# #) -> r) -> r
X x = Embed x

instance Category (Cat k con) where
  type Obj (Cat k con) = con
  id :: forall a. Obj (Cat k con) a => Cat k con a a
id = forall (k :: * -> * -> *) (con :: * -> Constraint) a. Cat k con a a
I
  Cat k con b c
I ∘ :: forall a b c.
(Obj (Cat k con) a, Obj (Cat k con) b, Obj (Cat k con) c) =>
Cat k con b c -> Cat k con a b -> Cat k con a c
∘ Cat k con a b
x = Cat k con a b
x
  Cat k con b c
x ∘ Cat k con a b
I = Cat k con b c
x
  Cat k con b c
x ∘ Cat k con a b
y = Cat k con b c
x forall (con :: * -> Constraint) a (k :: * -> * -> *) c a.
con a =>
Cat k con a c -> Cat k con a a -> Cat k con a c
:.: Cat k con a b
y

instance (ProdObj con, forall a b. (con a, con b) => con (a,b)) =>  Monoidal (Cat k con) where
  Cat k con a b
I × :: forall a b c d.
(Obj (Cat k con) a, Obj (Cat k con) b, Obj (Cat k con) c,
 Obj (Cat k con) d) =>
Cat k con a b -> Cat k con c d -> Cat k con (a ⊗ c) (b ⊗ d)
× Cat k con c d
I = forall (k :: * -> * -> *) (con :: * -> Constraint) a. Cat k con a a
I
  U' Unitor con b a
a × Cat k con c d
I = forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' (forall (con :: * -> Constraint) a b c.
(con a, con b, con c) =>
Unitor con a b -> Unitor con (a ⊗ c) (b, c)
IL Unitor con b a
a)
  Cat k con a b
I × U' Unitor con d c
a = forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' (forall (con :: * -> Constraint) a b c.
(con a, con b, con c) =>
Unitor con a b -> Unitor con (c, a) (c, b)
IR Unitor con d c
a)
  Cat k con a b
f × Cat k con c d
g = Cat k con a b
f forall (con :: * -> Constraint) a b c d (k :: * -> * -> *).
(con a, con b, con c, con d) =>
Cat k con a b -> Cat k con c d -> Cat k con (a ⊗ c) (b ⊗ d)
:×: Cat k con c d
g
  assoc :: forall a b c.
(Obj (Cat k con) a, Obj (Cat k con) b, Obj (Cat k con) c) =>
Cat k con ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
assoc =  forall (con :: * -> Constraint) a b c (k :: * -> * -> *).
(con a, con b, con c) =>
Cat k con ((a, b), c) (a, (b, c))
A
  assoc' :: forall a b c.
(Obj (Cat k con) a, Obj (Cat k con) b, Obj (Cat k con) c) =>
Cat k con (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
assoc' = forall (con :: * -> Constraint) a b c (k :: * -> * -> *).
(con a, con b, con c) =>
Cat k con (a, (b, c)) ((a, b), c)
A'
  swap :: forall a b.
(Obj (Cat k con) a, Obj (Cat k con) b) =>
Cat k con (a ⊗ b) (b ⊗ a)
swap = forall (con :: * -> Constraint) a b (k :: * -> * -> *).
(con a, con b) =>
Cat k con (a, b) (b, a)
S
  unitor :: forall a. Obj (Cat k con) a => Cat k con a (a ⊗ ())
unitor = forall (con :: * -> Constraint) a b (k :: * -> * -> *).
Unitor con a b -> Cat k con a b
U forall (con :: * -> Constraint) a. Unitor con a (a, ())
UR
  unitor' :: forall a. Obj (Cat k con) a => Cat k con (a ⊗ ()) a
unitor' = forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' forall (con :: * -> Constraint) a. Unitor con a (a, ())
UR


type Composer k con = forall a b c. (con a, con b, con c) => Cat k con b c -> Cat k con a b  -> Cat k con a c
type PartialComposer k con = forall a b c. (con a, con b, con c) => Cat k con b c -> Cat k con a b  -> Alt Maybe (Cat k con a c)
type ProtoSimplifier k con = (con (), ProdObj con, forall a b. (con a, con b) => con (a,b)) => Composer k con -> PartialComposer k con
type Simplifier k con = (con (), ProdObj con, forall a b. (con a, con b) => con (a,b)) => forall a b. (con a, con b) =>  Cat k con a b -> Cat k con a b

monoidalSimplify :: (con (), ProdObj con, forall α β. (con α, con β) => con (α,β)) => (con a, con b) => Cat k con a b -> Cat k con a b
monoidalSimplify :: forall (con :: * -> Constraint) a b (k :: * -> * -> *).
(con (), ProdObj con, forall α β. (con α, con β) => con (α, β),
 con a, con b) =>
Cat k con a b -> Cat k con a b
monoidalSimplify = forall (k :: * -> * -> *) (con :: * -> Constraint).
ProtoSimplifier k con -> Simplifier k con
mkSimplifier forall (k :: * -> * -> *) (con :: * -> Constraint).
ProtoSimplifier k con
monoidalRules

monoidalRules :: forall k con. ProtoSimplifier k con
monoidalRules :: forall (k :: * -> * -> *) (con :: * -> Constraint).
ProtoSimplifier k con
monoidalRules  Composer k con
(.) = \ Cat k con b c
x Cat k con a b
y -> forall {k} (f :: k -> *) (a :: k). f a -> Alt f a
Alt (forall a b c.
(con a, con b, con c) =>
Cat k con b c -> Cat k con a b -> Maybe (Cat k con a c)
after Cat k con b c
x Cat k con a b
y) where
  after :: (con a, con b, con c) => Cat k con b c -> Cat k con a b -> Maybe (Cat k con a c)

  -- obvious simplifications
  Cat k con b c
S after :: forall a b c.
(con a, con b, con c) =>
Cat k con b c -> Cat k con a b -> Maybe (Cat k con a c)
`after` Cat k con a b
S = forall a. a -> Maybe a
Just forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id
  Cat k con b c
A' `after` Cat k con a b
A = forall a. a -> Maybe a
Just forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id
  Cat k con b c
A `after` Cat k con a b
A' = forall a. a -> Maybe a
Just forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id

  -- commute (or cancel) unitors
  U' Unitor con c b
x `after` U Unitor con a b
y = forall a. a -> Maybe a
Just (forall (con :: * -> Constraint) a b c (cat :: * -> * -> *).
(ProdObj con, forall α β. (con α, con β) => con (α, β), con (),
 con a, con b) =>
Unitor con c b -> Unitor con a b -> Cat cat con a c
commuteUnitors Unitor con c b
x Unitor con a b
y)

  -- push swaps to the right
  Cat k con b c
S `after` (Cat k con a b
f :×: Cat k con c d
g) = forall a. a -> Maybe a
Just ((Cat k con c d
g forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× Cat k con a b
f) Composer k con
. forall (con :: * -> Constraint) a b (k :: * -> * -> *).
(con a, con b) =>
Cat k con (a, b) (b, a)
S)

  -- swap individual strands
  Cat k con b c
S `after` Cat k con a b
A = forall a. a -> Maybe a
Just (forall (k :: * -> * -> *) a b c.
(Monoidal k, Obj k a, Obj k b, Obj k c) =>
k (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
assoc' Composer k con
. (forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap) Composer k con
. forall (k :: * -> * -> *) a b c.
(Monoidal k, Obj k a, Obj k b, Obj k c) =>
k ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
assoc Composer k con
. (forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id))
  Cat k con b c
S `after` Cat k con a b
A' = forall a. a -> Maybe a
Just (forall (k :: * -> * -> *) a b c.
(Monoidal k, Obj k a, Obj k b, Obj k c) =>
k ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
assoc Composer k con
. (forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id) Composer k con
. forall (k :: * -> * -> *) a b c.
(Monoidal k, Obj k a, Obj k b, Obj k c) =>
k (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
assoc' Composer k con
. (forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap))
  Cat k con b c
A  `after` Cat k con a b
S = forall a. a -> Maybe a
Just ((forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap) Composer k con
. forall (k :: * -> * -> *) a b c.
(Monoidal k, Obj k a, Obj k b, Obj k c) =>
k ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
assoc  Composer k con
. (forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id) Composer k con
. forall (k :: * -> * -> *) a b c.
(Monoidal k, Obj k a, Obj k b, Obj k c) =>
k (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
assoc')
  Cat k con b c
A' `after` Cat k con a b
S = forall a. a -> Maybe a
Just ((forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id) Composer k con
. forall (k :: * -> * -> *) a b c.
(Monoidal k, Obj k a, Obj k b, Obj k c) =>
k (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
assoc'  Composer k con
. (forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap ) Composer k con
. forall (k :: * -> * -> *) a b c.
(Monoidal k, Obj k a, Obj k b, Obj k c) =>
k ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
assoc)

  -- push U' through S
  U' Unitor con c b
UR `after` Cat k con a b
S = forall a. a -> Maybe a
Just (forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' forall (con :: * -> Constraint) a. Unitor con a ((), a)
UL)
  U' Unitor con c b
UL `after` Cat k con a b
S = forall a. a -> Maybe a
Just (forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' forall (con :: * -> Constraint) a. Unitor con a (a, ())
UR)
  U' (IL Unitor con a b
a) `after` Cat k con a b
S = forall a. a -> Maybe a
Just (forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap Composer k con
. forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' (forall (con :: * -> Constraint) a b c.
(con a, con b, con c) =>
Unitor con a b -> Unitor con (c, a) (c, b)
IR Unitor con a b
a))
  U' (IR Unitor con a b
a) `after` Cat k con a b
S = forall a. a -> Maybe a
Just (forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap Composer k con
. forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' (forall (con :: * -> Constraint) a b c.
(con a, con b, con c) =>
Unitor con a b -> Unitor con (a ⊗ c) (b, c)
IL Unitor con a b
a))

  -- push U' into ×
  U' Unitor con c b
UR `after` ((Cat k con a b
f :×: Cat k con c d
I) :<: Cat k con a b
h) = forall a. a -> Maybe a
Just (Cat k con a b
f Composer k con
. forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' forall (con :: * -> Constraint) a. Unitor con a (a, ())
UR  Composer k con
. Cat k con a b
h)
  U' (IL Unitor con a b
a) `after` ((Cat k con a b
f :×: Cat k con c d
g) :<: Cat k con a b
h) = forall a. a -> Maybe a
Just (((forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con a b
a Composer k con
. Cat k con a b
f) forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× Cat k con c d
g)  Composer k con
. Cat k con a b
h )
  U' (IR Unitor con a b
a) `after` ((Cat k con a b
f :×: Cat k con c d
g) :<: Cat k con a b
h) = forall a. a -> Maybe a
Just ((Cat k con a b
f forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× (forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con a b
a Composer k con
. Cat k con c d
g))  Composer k con
. Cat k con a b
h )

  -- push U' through A'
  U' Unitor con c b
UR `after` Cat k con a b
A' = forall a. a -> Maybe a
Just (forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' forall (con :: * -> Constraint) a. Unitor con a (a, ())
UR)
  U' (IR Unitor con a b
a) `after` Cat k con a b
A' = forall a. a -> Maybe a
Just (forall (con :: * -> Constraint) a b c (k :: * -> * -> *).
(con a, con b, con c) =>
Cat k con (a, (b, c)) ((a, b), c)
A' Composer k con
. (forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× (forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con a b
a)))
  U' (IL (IR Unitor con a b
a)) `after` Cat k con a b
A' = forall a. a -> Maybe a
Just (forall (con :: * -> Constraint) a b c (k :: * -> * -> *).
(con a, con b, con c) =>
Cat k con (a, (b, c)) ((a, b), c)
A' Composer k con
. (forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× (forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con a b
a forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id)) )
  U' (IL Unitor con a b
UR) `after` Cat k con a b
A' = forall a. a -> Maybe a
Just (forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' forall (con :: * -> Constraint) a. Unitor con a ((), a)
UL )
  U' (IL Unitor con a b
UL)     `after` Cat k con a b
A' = forall a. a -> Maybe a
Just (forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' forall (con :: * -> Constraint) a. Unitor con a ((), a)
UL)
  U' (IL (IL Unitor con a b
a)) `after` Cat k con a b
A' = forall a. a -> Maybe a
Just (forall (con :: * -> Constraint) a b c (k :: * -> * -> *).
(con a, con b, con c) =>
Cat k con (a, (b, c)) ((a, b), c)
A' Composer k con
. (forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con a b
a forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id))

  -- push U' through A
  U' Unitor con c b
UL          `after` Cat k con a b
A = forall a. a -> Maybe a
Just (forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' forall (con :: * -> Constraint) a. Unitor con a ((), a)
UL forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id)
  U' (IL Unitor con a b
a)      `after` Cat k con a b
A = forall a. a -> Maybe a
Just (forall (con :: * -> Constraint) a b c (k :: * -> * -> *).
(con a, con b, con c) =>
Cat k con ((a, b), c) (a, (b, c))
A Composer k con
. ((forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con a b
a forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id) forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id))
  U' (IR (IL Unitor con a b
a)) `after` Cat k con a b
A = forall a. a -> Maybe a
Just (forall (con :: * -> Constraint) a b c (k :: * -> * -> *).
(con a, con b, con c) =>
Cat k con ((a, b), c) (a, (b, c))
A Composer k con
. ((forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con a b
a) forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id))
  U' (IR Unitor con a b
UL)     `after` Cat k con a b
A = forall a. a -> Maybe a
Just (forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' forall (con :: * -> Constraint) a. Unitor con a (a, ())
UR forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id)
  U' (IR Unitor con a b
UR)     `after` Cat k con a b
A = forall a. a -> Maybe a
Just (forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' forall (con :: * -> Constraint) a. Unitor con a (a, ())
UR)
  U' (IR (IR Unitor con a b
a)) `after` Cat k con a b
A = forall a. a -> Maybe a
Just (forall (con :: * -> Constraint) a b c (k :: * -> * -> *).
(con a, con b, con c) =>
Cat k con ((a, b), c) (a, (b, c))
A Composer k con
. (forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con a b
a))

  -- compose strands 
  (Cat k con a b
f :×: Cat k con c d
g) `after` (Cat k con a b
h :×: Cat k con c d
i) = forall a. a -> Maybe a
Just ((Cat k con a b
f Composer k con
. Cat k con a b
h) forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× (Cat k con c d
g Composer k con
. Cat k con c d
i))


  -- failing the above, extract unitors
  ((Cat k con b b
f :>: U' Unitor con b a
a) :×: Cat k con c d
g) `after` Cat k con a b
h = forall a. a -> Maybe a
Just ((Cat k con b b
fforall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
×Cat k con c d
g) Composer k con
. forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' (forall (con :: * -> Constraint) a b c.
(con a, con b, con c) =>
Unitor con a b -> Unitor con (a ⊗ c) (b, c)
IL Unitor con b a
a) Composer k con
. Cat k con a b
h )
  (Cat k con a b
f :×: (Cat k con b d
g :>: U' Unitor con b c
a)) `after` Cat k con a b
h = forall a. a -> Maybe a
Just ((Cat k con a b
f forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× Cat k con b d
g) Composer k con
. forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' (forall (con :: * -> Constraint) a b c.
(con a, con b, con c) =>
Unitor con a b -> Unitor con (c, a) (c, b)
IR Unitor con b c
a) Composer k con
. Cat k con a b
h)

  Cat k con b c
h `after` ((Cat k con b b
f :>: U' Unitor con b a
a) :×: Cat k con c d
g) = forall a. a -> Maybe a
Just (Cat k con b c
h Composer k con
. (Cat k con b b
f forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× Cat k con c d
g) Composer k con
. forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' (forall (con :: * -> Constraint) a b c.
(con a, con b, con c) =>
Unitor con a b -> Unitor con (a ⊗ c) (b, c)
IL Unitor con b a
a) )
  Cat k con b c
h `after` (Cat k con a b
f :×: (Cat k con b d
g :>: U' Unitor con b c
a)) = forall a. a -> Maybe a
Just (Cat k con b c
h Composer k con
. (Cat k con a b
f forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× Cat k con b d
g) Composer k con
. forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' (forall (con :: * -> Constraint) a b c.
(con a, con b, con c) =>
Unitor con a b -> Unitor con (c, a) (c, b)
IR Unitor con b c
a) )


  -- extract unitors from ▵:
  -- h `after` ((U a :<: f) :▵: g) = Just (h . U (IL a) . (f ▵ g)  )
  -- h `after` (f :▵: (U a :<: g )) = Just (h . U (IR a) . (f ▵ g) )

  Cat k con b c
_ `after` Cat k con a b
_ = forall a. Maybe a
Nothing


neverEqual :: Comparator k
neverEqual :: forall {k} {k} (k :: k -> k -> *). Comparator k
neverEqual k a b
_ k a b'
_ = forall a. Maybe a
Nothing


mkSimplifier :: forall k con. ProtoSimplifier k con -> Simplifier k con
mkSimplifier :: forall (k :: * -> * -> *) (con :: * -> Constraint).
ProtoSimplifier k con -> Simplifier k con
mkSimplifier ProtoSimplifier k con
protoAfter = forall a b. (con a, con b) => Cat k con a b -> Cat k con a b
simplify where
   (...) :: Composer k con
   Cat k con b c
I ... :: Composer k con
... Cat k con a b
g  = Cat k con a b
g -- g is already normal.
   Cat k con b c
f ... Cat k con a b
I  = Cat k con b c
f -- f is already normal.
   (Cat k con b c
f :>: Cat k con b b
g) ... (Cat k con b b
h :<: Cat k con a b
i) = case forall {k} (f :: k -> *) (a :: k). Alt f a -> f a
getAlt (Cat k con b b
g PartialComposer k con
`after` Cat k con b b
h) of
     Maybe (Cat k con b b)
Nothing -> (Cat k con b c
f forall (obj :: * -> Constraint) x y (k :: * -> * -> *) b.
(obj x, obj y, obj b) =>
Cat k obj b y -> Cat k obj x b -> Cat k obj x y
:>: Cat k con b b
g) forall (con :: * -> Constraint) a (k :: * -> * -> *) c a.
con a =>
Cat k con a c -> Cat k con a a -> Cat k con a c
:.: (Cat k con b b
h forall (obj :: * -> Constraint) x y (k :: * -> * -> *) b.
(obj x, obj y, obj b) =>
Cat k obj b y -> Cat k obj x b -> Cat k obj x y
:<: Cat k con a b
i) -- no reaction.  both subterms are normal. so we're done.
     Just Cat k con b b
j -> Cat k con b c
f Composer k con
... Cat k con b b
j Composer k con
... Cat k con a b
i --- reaction :: we must recurse. ("After" must return a normal term; j.)
   Cat k con b c
f ... Cat k con a b
g = Cat k con b c
f forall (con :: * -> Constraint) a (k :: * -> * -> *) c a.
con a =>
Cat k con a c -> Cat k con a a -> Cat k con a c
:.: Cat k con a b
g
   after :: PartialComposer k con
   after :: PartialComposer k con
after = ProtoSimplifier k con
protoAfter Composer k con
(...)

   simplify :: (con a, con b) => Cat k con a b -> Cat k con a b
   -- simplify (Curry f) = Curry (simplify f)
   simplify :: forall a b. (con a, con b) => Cat k con a b -> Cat k con a b
simplify (Cat k con a b
f :×: Cat k con c d
g) = forall a b. (con a, con b) => Cat k con a b -> Cat k con a b
simplify Cat k con a b
f forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall a b. (con a, con b) => Cat k con a b -> Cat k con a b
simplify Cat k con c d
g
   simplify (Cat k con b b
f :.: Cat k con a b
g) = forall a b. (con a, con b) => Cat k con a b -> Cat k con a b
simplify Cat k con b b
f Composer k con
... forall a b. (con a, con b) => Cat k con a b -> Cat k con a b
simplify Cat k con a b
g
   simplify Cat k con a b
x = Cat k con a b
x


toDup :: (ProdObj con, forall x y. (con x, con y) => con (x,y), con (), con a, con b) => Cat k con a b -> Cat k con a b
toDup :: forall (con :: * -> Constraint) a b (k :: * -> * -> *).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con a, con b) =>
Cat k con a b -> Cat k con a b
toDup = \case
  Cat k con a b
I -> forall (k :: * -> * -> *) (con :: * -> Constraint) a. Cat k con a a
I
  (Cat k con a b
f :×: Cat k con c d
g) -> forall (con :: * -> Constraint) a b (k :: * -> * -> *).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con a, con b) =>
Cat k con a b -> Cat k con a b
toDup Cat k con a b
f forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (con :: * -> Constraint) a b (k :: * -> * -> *).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con a, con b) =>
Cat k con a b -> Cat k con a b
toDup Cat k con c d
g
  (Cat k con b b
f :.: Cat k con a b
g) -> forall (con :: * -> Constraint) a b (k :: * -> * -> *).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con a, con b) =>
Cat k con a b -> Cat k con a b
toDup Cat k con b b
f forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall (con :: * -> Constraint) a b (k :: * -> * -> *).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con a, con b) =>
Cat k con a b -> Cat k con a b
toDup Cat k con a b
g
  X k a b
ϕ -> forall (k :: * -> * -> *) (con :: * -> Constraint) a b.
(con a, con b) =>
k a b -> Cat k con a b
X k a b
ϕ
  Cat k con a b
A -> forall (con :: * -> Constraint) a b c (k :: * -> * -> *).
(con a, con b, con c) =>
Cat k con ((a, b), c) (a, (b, c))
A
  Cat k con a b
A' -> forall (con :: * -> Constraint) a b c (k :: * -> * -> *).
(con a, con b, con c) =>
Cat k con (a, (b, c)) ((a, b), c)
A'
  Cat k con a b
S -> forall (con :: * -> Constraint) a b (k :: * -> * -> *).
(con a, con b) =>
Cat k con (a, b) (b, a)
S
  (U Unitor con a b
u) -> forall (con :: * -> Constraint) a b (k :: * -> * -> *).
Unitor con a b -> Cat k con a b
U Unitor con a b
u
  (U' Unitor con b a
u) -> forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con b a
u


toE :: (ProdObj con, forall x y. (con x, con y) => con (x,y), con (), con a, con b) => Cat k con a b -> Cat k con a b
toE :: forall (con :: * -> Constraint) a b (k :: * -> * -> *).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con a, con b) =>
Cat k con a b -> Cat k con a b
toE = \case
  Cat k con a b
I -> forall (k :: * -> * -> *) (con :: * -> Constraint) a. Cat k con a a
I
  (Cat k con a b
f :×: Cat k con c d
g) -> forall (con :: * -> Constraint) a b (k :: * -> * -> *).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con a, con b) =>
Cat k con a b -> Cat k con a b
toE Cat k con a b
f forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (con :: * -> Constraint) a b (k :: * -> * -> *).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con a, con b) =>
Cat k con a b -> Cat k con a b
toE Cat k con c d
g
  (Cat k con b b
f :.: Cat k con a b
g) -> forall (con :: * -> Constraint) a b (k :: * -> * -> *).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con a, con b) =>
Cat k con a b -> Cat k con a b
toE Cat k con b b
f forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall (con :: * -> Constraint) a b (k :: * -> * -> *).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con a, con b) =>
Cat k con a b -> Cat k con a b
toE Cat k con a b
g
  X k a b
ϕ -> forall (k :: * -> * -> *) (con :: * -> Constraint) a b.
(con a, con b) =>
k a b -> Cat k con a b
X k a b
ϕ
  Cat k con a b
A -> forall (con :: * -> Constraint) a b c (k :: * -> * -> *).
(con a, con b, con c) =>
Cat k con ((a, b), c) (a, (b, c))
A
  Cat k con a b
A' -> forall (con :: * -> Constraint) a b c (k :: * -> * -> *).
(con a, con b, con c) =>
Cat k con (a, (b, c)) ((a, b), c)
A'
  Cat k con a b
S -> forall (con :: * -> Constraint) a b (k :: * -> * -> *).
(con a, con b) =>
Cat k con (a, b) (b, a)
S
  (U Unitor con a b
u) -> forall (con :: * -> Constraint) a b (k :: * -> * -> *).
Unitor con a b -> Cat k con a b
U Unitor con a b
u
  (U' Unitor con b a
u) -> forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con b a
u