{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# OPTIONS_GHC -Wno-incomplete-patterns -Wno-overlapping-patterns #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TupleSections #-}
{-# 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

data 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). String -> Sho a b
shoCon String
name = (Int -> ShowS) -> Sho a b
forall {k} {k} (a :: k) (b :: k). (Int -> ShowS) -> Sho a b
Sho ((Int -> ShowS) -> Sho a b) -> (Int -> ShowS) -> Sho a b
forall a b. (a -> b) -> a -> b
$ \Int
_ -> String -> ShowS
showString String
name

instance Category Sho where
  type Obj Sho = Trivial
  id :: forall a. Obj Sho a => Sho a a
id = String -> Sho a a
forall {k} {k} (a :: k) (b :: k). String -> Sho a b
shoCon String
"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 = (Int -> ShowS) -> Sho a c
forall {k} {k} (a :: k) (b :: k). (Int -> ShowS) -> Sho a b
Sho ((Int -> ShowS) -> Sho a c) -> (Int -> ShowS) -> Sho a c
forall a b. (a -> b) -> a -> b
$ \Int
d -> Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0) (Int -> ShowS
f Int
0 ShowS -> ShowS -> ShowS
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. String -> ShowS
showString String
" ∘ " ShowS -> ShowS -> ShowS
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 = String -> Sho (a ⊗ b) (b ⊗ a)
forall {k} {k} (a :: k) (b :: k). String -> Sho a b
shoCon String
"swap"
  assoc :: forall a b c.
(Obj Sho a, Obj Sho b, Obj Sho c) =>
Sho ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
assoc = String -> Sho ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
forall {k} {k} (a :: k) (b :: k). String -> Sho a b
shoCon String
"assoc"
  assoc' :: forall a b c.
(Obj Sho a, Obj Sho b, Obj Sho c) =>
Sho (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
assoc' = String -> Sho (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
forall {k} {k} (a :: k) (b :: k). String -> Sho a b
shoCon String
"assoc'"
  unitor :: forall a. Obj Sho a => Sho a (a ⊗ ())
unitor = String -> Sho a (a ⊗ ())
forall {k} {k} (a :: k) (b :: k). String -> Sho a b
shoCon String
"unitor"
  unitor' :: forall a. Obj Sho a => Sho (a ⊗ ()) a
unitor' = String -> Sho (a ⊗ ()) a
forall {k} {k} (a :: k) (b :: k). String -> Sho a b
shoCon String
"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 = (Int -> ShowS) -> Sho (a ⊗ c) (b ⊗ d)
forall {k} {k} (a :: k) (b :: k). (Int -> ShowS) -> Sho a b
Sho ((Int -> ShowS) -> Sho (a ⊗ c) (b ⊗ d))
-> (Int -> ShowS) -> Sho (a ⊗ c) (b ⊗ d)
forall a b. (a -> b) -> a -> b
$ \Int
d -> Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0) (Int -> ShowS
f Int
2 ShowS -> ShowS -> ShowS
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. String -> ShowS
showString String
" × " ShowS -> ShowS -> ShowS
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 = String -> Sho a ()
forall {k} {k} (a :: k) (b :: k). String -> Sho a b
shoCon String
"dis"
  dup :: forall a. (Obj Sho a, Obj Sho (a ⊗ a)) => Sho a (a ⊗ a)
dup = String -> Sho a (a ⊗ a)
forall {k} {k} (a :: k) (b :: k). String -> Sho a b
shoCon String
"dup"
  exl :: forall a b. O2 Sho a b => Sho (a ⊗ b) a
exl = String -> Sho (a ⊗ b) a
forall {k} {k} (a :: k) (b :: k). String -> Sho a b
shoCon String
"exl"
  exr :: forall a b. O2 Sho a b => Sho (a ⊗ b) b
exr = String -> Sho (a ⊗ b) b
forall {k} {k} (a :: k) (b :: k). String -> Sho a b
shoCon String
"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 = (Int -> ShowS) -> Sho a (b ⊗ c)
forall {k} {k} (a :: k) (b :: k). (Int -> ShowS) -> Sho a b
Sho ((Int -> ShowS) -> Sho a (b ⊗ c))
-> (Int -> ShowS) -> Sho a (b ⊗ c)
forall a b. (a -> b) -> a -> b
$ \Int
d -> Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0) (Int -> ShowS
f Int
2 ShowS -> ShowS -> ShowS
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. String -> ShowS
showString String
" ▵ " ShowS -> ShowS -> ShowS
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 = Sho a b -> Sho a b
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 -> String
show Cat k con a b
x = Int -> Cat k con a b -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (-Int
1) Cat k con a b
x String
""
  showsPrec :: Int -> Cat k con a b -> ShowS
showsPrec Int
d = \case
    Cat k con a b
I -> String -> ShowS
showString String
"id"
    Cat k con a b
S -> String -> ShowS
showString String
"swap"
    Cat k con a b
A  -> String -> ShowS
showString String
"assoc"
    Cat k con a b
A' -> String -> ShowS
showString String
"assoc'"
    U Unitor con a b
a -> {-showString "[" .-} Sho a b -> Int -> ShowS
forall {k} {k} (a :: k) (b :: k). Sho a b -> Int -> ShowS
fromSho (Unitor (Obj Sho) a b -> Sho a b
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 con a b -> Unitor Trivial a b
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 "[" .-} Sho a b -> Int -> ShowS
forall {k} {k} (a :: k) (b :: k). Sho a b -> Int -> ShowS
fromSho (Unitor (Obj Sho) b a -> Sho a b
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 con b a -> Unitor Trivial b a
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 -> String -> ShowS
showString (k a b -> String
forall a. Show a => a -> String
show k a b
s)
    Cat k con b b
f :.: Cat k con a b
g -> Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>  Int
0) (Int -> Cat k con b b -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 Cat k con b b
f ShowS -> ShowS -> ShowS
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. String -> ShowS
showString String
" ∘ " ShowS -> ShowS -> ShowS
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. Int -> Cat k con a b -> ShowS
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> -Int
1) (Int -> Cat k con a b -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
2 Cat k con a b
f ShowS -> ShowS -> ShowS
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. String -> ShowS
showString String
" × " ShowS -> ShowS -> ShowS
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. Int -> Cat k con c d -> ShowS
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
_ -> String -> ShowS
showString String
"?"

    Cat k con a b
I -> String -> ShowS
showString String
"id"
    Cat k con b b
f :.: Cat k con a b
g -> Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0) (Int -> Cat k con b b -> ShowS
forall (k :: * -> * -> *) (con :: * -> Constraint) a b.
Int -> Cat k con a b -> ShowS
showDbg Int
0 Cat k con b b
f ShowS -> ShowS -> ShowS
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. String -> ShowS
showString String
" ∘ " ShowS -> ShowS -> ShowS
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. Int -> Cat k con a b -> ShowS
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 (Int -> Cat k con a b -> ShowS
forall (k :: * -> * -> *) (con :: * -> Constraint) a b.
Int -> Cat k con a b -> ShowS
showDbg Int
2 Cat k con a b
f ShowS -> ShowS -> ShowS
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. String -> ShowS
showString String
" × " ShowS -> ShowS -> ShowS
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. Int -> Cat k con c d -> ShowS
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 -> String -> ShowS
showString String
"σ"
    Cat k con a b
A  -> String -> ShowS
showString String
"α"
    Cat k con a b
A' -> String -> ShowS
showString String
"α'"
    U Unitor con a b
_ -> String -> ShowS
showString String
"ρ"
    U' Unitor con b a
a  -> String -> ShowS
showString (String
"ρ'(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Unitor con b a -> String
forall a. Show a => a -> String
show Unitor con b a
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")")



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

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 -> k' a b -> Cat k' con a b
forall (k :: * -> * -> *) (con :: * -> Constraint) a b.
(con a, con b) =>
k a b -> Cat k con a b
X (k a b -> k' a b
forall x y. (con x, con y) => k x y -> k' x y
f k a b
g)

  Cat k con a b
I -> Cat k' con a b
forall (k :: * -> * -> *) (con :: * -> Constraint) a. Cat k con a a
I
  Cat k con b b
a :.: Cat k con a b
b -> (forall x y. (con x, con y) => k x y -> k' x y)
-> Cat k con b b -> Cat k' con 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 Cat k' con b b -> Cat k' con a b -> Cat k' con a 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
:.: (forall x y. (con x, con y) => k x y -> k' x y)
-> Cat k con a b -> Cat k' con a 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
b

  Cat k con a b
a :×: Cat k con c d
b -> (forall x y. (con x, con y) => k x y -> k' x y)
-> Cat k con a b -> Cat k' con a 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 Cat k' con a b -> Cat k' con c d -> Cat k' con (a, c) (b, d)
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 x y. (con x, con y) => k x y -> k' x y)
-> Cat k con c d -> Cat k' con c 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 -> Cat k' con a b
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' -> Cat k' con a b
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 -> Cat k' con a b
forall (con :: * -> Constraint) a b (k :: * -> * -> *).
(con a, con b) =>
Cat k con (a, b) (b, a)
S
  U Unitor con a b
x -> Unitor con a b -> Cat k' con a b
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 -> Unitor con b a -> Cat k' con a b
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 -> String -> Cat k' con a b
forall a. HasCallStack => String -> a
error (Int -> Cat k con a b -> ShowS
forall (k :: * -> * -> *) (con :: * -> Constraint) a b.
Int -> Cat k con a b -> ShowS
showDbg Int
0 Cat k con a b
x String
" (Free.mapGenerators)")


instance Show (Unitor con a b) where
  show :: Unitor con a b -> String
show Unitor con a b
UL = String
"⟨"
  show Unitor con a b
UR = String
"⟩"
  show (IL Unitor con a b
a) = String
"⟨" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Unitor con a b -> String
forall a. Show a => a -> String
show Unitor con a b
a
  show (IR Unitor con a b
a) = String
"⟩" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Unitor con a b -> String
forall a. Show a => a -> String
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 = (b :~: b) -> Maybe (b :~: b)
forall a. a -> Maybe a
Just b :~: b
forall {k} (a :: k). a :~: a
Refl
compareUnitors Unitor con a b
UR Unitor con a b'
UR = (b :~: b) -> Maybe (b :~: b)
forall a. a -> Maybe a
Just b :~: b
forall {k} (a :: k). a :~: a
Refl
compareUnitors (IL Unitor con a b
a) (IL Unitor con a b
b) = case Unitor con a b -> Unitor con a b -> Maybe (b :~: b)
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
Unitor con a b
b of Maybe (b :~: b)
Nothing -> Maybe (b :~: b')
forall a. Maybe a
Nothing; Just b :~: b
Refl -> (b :~: b) -> Maybe (b :~: b)
forall a. a -> Maybe a
Just b :~: b
forall {k} (a :: k). a :~: a
Refl
compareUnitors (IR Unitor con a b
a) (IR Unitor con a b
b) = case Unitor con a b -> Unitor con a b -> Maybe (b :~: b)
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
Unitor con a b
b of Maybe (b :~: b)
Nothing -> Maybe (b :~: b')
forall a. Maybe a
Nothing; Just b :~: b
Refl -> (b :~: b) -> Maybe (b :~: b)
forall a. a -> Maybe a
Just b :~: b
forall {k} (a :: k). a :~: a
Refl
compareUnitors Unitor con a b
_ Unitor con a b'
_ = Maybe (b :~: 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 = Unitor Trivial a b
forall (con :: * -> Constraint) a. Unitor con a ((), a)
UL
trivializeUnitor Unitor con a b
UR = Unitor Trivial a b
forall (con :: * -> Constraint) a. Unitor con a (a, ())
UR
trivializeUnitor (IL Unitor con a b
f) = Unitor Trivial a b -> Unitor Trivial (a, c) (b, c)
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 -> Unitor Trivial a b
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) = Unitor Trivial a b -> Unitor Trivial (c, a) (c, b)
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 -> Unitor Trivial a b
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 = Cat cat con a c
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id
commuteUnitors Unitor con c b
UL Unitor con a b
UR = Cat cat con a c
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id
commuteUnitors Unitor con c b
UR Unitor con a b
UR = Cat cat con a c
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id
commuteUnitors Unitor con c b
UR Unitor con a b
UL = Cat cat con a c
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) = (Unitor con a b -> Unitor con a b -> Cat cat con a a
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
Unitor con a b
b Cat cat con a a -> Cat cat con c c -> Cat cat con (a ⊗ c) (a, c)
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 cat con c c
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) = (Cat cat con c c
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id Cat cat con c c -> Cat cat con a a -> Cat cat con (c ⊗ a) (c, 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)
× Unitor con a b -> Unitor con a b -> Cat cat con a a
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
Unitor con a b
b)
commuteUnitors (IR Unitor con a b
a) (IL Unitor con a b
b) = (Unitor con (a, a) (b, a) -> Cat cat con (a, a) (b, a)
forall (con :: * -> Constraint) a b (k :: * -> * -> *).
Unitor con a b -> Cat k con a b
U (Unitor con a b -> Unitor con (a, a) (b, a)
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)) Cat cat con (a, a) (b, a)
-> Cat cat con (a, b) (a, a) -> Cat cat con (a, b) (b, a)
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
.  (Unitor con (a, a) (a, b) -> Cat cat con (a, b) (a, a)
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' (Unitor con a b -> Unitor con (a, a) (a, b)
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) = (Unitor con (a, a) (a, b) -> Cat cat con (a, a) (a, b)
forall (con :: * -> Constraint) a b (k :: * -> * -> *).
Unitor con a b -> Cat k con a b
U (Unitor con a b -> Unitor con (a, a) (a, b)
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)) Cat cat con (a, a) (a, b)
-> Cat cat con (b, a) (a, a) -> Cat cat con (b, a) (a, b)
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
.  (Unitor con (a, a) (b, a) -> Cat cat con (b, a) (a, a)
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' (Unitor con a b -> Unitor con (a, a) (b, a)
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) = Unitor con a b -> Cat cat con a b
forall (con :: * -> Constraint) a b (k :: * -> * -> *).
Unitor con a b -> Cat k con a b
U Unitor con a b
a Cat cat con a b -> Cat cat con ((), a) a -> Cat cat con ((), a) b
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. Unitor con a ((), a) -> Cat cat con ((), a) a
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con a ((), a)
forall (con :: * -> Constraint) a. Unitor con a ((), a)
UL
commuteUnitors Unitor con c b
UR (IL Unitor con a b
a) = Unitor con a b -> Cat cat con a b
forall (con :: * -> Constraint) a b (k :: * -> * -> *).
Unitor con a b -> Cat k con a b
U Unitor con a b
a Cat cat con a b -> Cat cat con (a, ()) a -> Cat cat con (a, ()) b
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. Unitor con a (a, ()) -> Cat cat con (a, ()) a
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con a (a, ())
forall (con :: * -> Constraint) a. Unitor con a (a, ())
UR
commuteUnitors (IR Unitor con a b
a) Unitor con a b
UL = Unitor con a ((), a) -> Cat cat con a ((), a)
forall (con :: * -> Constraint) a b (k :: * -> * -> *).
Unitor con a b -> Cat k con a b
U Unitor con a ((), a)
forall (con :: * -> Constraint) a. Unitor con a ((), a)
UL Cat cat con a ((), a) -> Cat cat con b a -> Cat cat con b ((), a)
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. Unitor con a b -> Cat cat con b a
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 = Unitor con a (a, ()) -> Cat cat con a (a, ())
forall (con :: * -> Constraint) a b (k :: * -> * -> *).
Unitor con a b -> Cat k con a b
U Unitor con a (a, ())
forall (con :: * -> Constraint) a. Unitor con a (a, ())
UR Cat cat con a (a, ()) -> Cat cat con b a -> Cat cat con b (a, ())
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. Unitor con a b -> Cat cat con b a
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 -> Cat k con b a
forall (k :: * -> * -> *) (con :: * -> Constraint) a. Cat k con a a
I
    Cat k con a b
f :×: Cat k con c d
g -> Cat k con a b -> Cat k con b a
forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Invertible k =>
k a b -> k b a
dual Cat k con a b
f Cat k con b a -> Cat k con d c -> Cat k con (b, d) (a, c)
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 -> Cat k con d c
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 -> Cat k con a b -> Cat k con b a
forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Invertible k =>
k a b -> k b a
dual Cat k con a b
g Cat k con b a -> Cat k con b b -> Cat k con 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
:.: Cat k con b b -> Cat k con b b
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 -> Cat k con b a
forall (con :: * -> Constraint) a b (k :: * -> * -> *).
(con a, con b) =>
Cat k con (a, b) (b, a)
S
    Cat k con a b
A -> Cat k con 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' -> Cat k con 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 :.: (Cat k obj x b -> Cat k obj x b
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 Cat k obj b y -> Cat k obj b b -> Cat k obj b y
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) Cat k obj b y -> Cat k obj x b -> Cat k obj x y
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 (Cat k obj a c -> Cat k obj a c
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 Cat k obj b c -> Cat k obj a b -> Cat k obj a c
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 = Cat k obj c c
forall (k :: * -> * -> *) (con :: * -> Constraint) a. Cat k con a a
I Cat k obj c c -> Cat k obj a c -> Cat k obj a c
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 ((Cat k obj b y -> Cat k obj b y
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 Cat k obj b y -> Cat k obj x b -> Cat k obj x y
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 Cat k obj b b -> Cat k obj x b -> Cat k obj x 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 (Cat k obj a c -> Cat k obj a c
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 Cat k obj b c -> Cat k obj a b -> Cat k obj a c
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 Cat k obj a c -> Cat k obj a a -> Cat k obj a c
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 a
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)
-> (Void# -> 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 Cat k obj b y -> Cat k obj x b -> Cat k obj x y
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)
-> (Void# -> 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 Cat k obj b y -> Cat k obj x b -> Cat k obj x y
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          = k a b
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)  = Cat k (Obj k) a b -> k a b
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 k a b -> k c d -> k (a, c) (b, d)
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 (Obj k) c d -> k c 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)  = Cat k (Obj k) b b -> k b b
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 k b b -> k a b -> k a b
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. Cat k (Obj k) a b -> k a b
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          = k a b
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'         = k a b
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          = k a b
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)      = Unitor (Obj k) a b -> k a b
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)     = Unitor (Obj k) b a -> k a b
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 -> k a b
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) -> Cat k (Obj k) a b -> k a b
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 k a b -> k c d -> k (a, c) (b, d)
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 (Obj k) c d -> k c 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) -> Cat k (Obj k) b b -> k b b
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 k b b -> k a b -> k a b
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. Cat k (Obj k) a b -> k a b
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 -> k a b
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' -> k a b
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 -> k a b
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) -> Unitor (Obj k) a b -> k a b
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) -> Unitor (Obj k) b a -> k a b
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 = k a b
forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k a (a ⊗ ())
unitor
evalUnitor Unitor (Obj k) a b
UL = k (a, ()) ((), a)
forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap k (a, ()) ((), a) -> k a (a, ()) -> k a ((), a)
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. k a (a, ())
forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k a (a ⊗ ())
unitor
evalUnitor (IL Unitor (Obj k) a b
x) = (Unitor (Obj k) a b -> k a b
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 k a b -> k c c -> k (a, c) (b, c)
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)
× k c c
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id)
evalUnitor (IR Unitor (Obj k) a b
x) = (k c c
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id k c c -> k a b -> k (c, a) (c, 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)
× Unitor (Obj k) a b -> k a b
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 = k a b
forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k (a ⊗ ()) a
unitor'
evalUnitor' Unitor (Obj k) b a
UL = k (b, ()) b
forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k (a ⊗ ()) a
unitor' k (b, ()) b -> k ((), b) (b, ()) -> k ((), b) b
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. k ((), b) (b, ())
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) = (Unitor (Obj k) a b -> k b a
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 k b a -> k c c -> k (b, c) (a, c)
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)
× k c c
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id)
evalUnitor' (IR Unitor (Obj k) a b
x) = (k c c
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id k c c -> k b a -> k (c, b) (c, 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)
× Unitor (Obj k) a b -> k b a
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) -> (Void# -> 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 = Cat k con a a
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
Cat k con a c
x
  Cat k con b c
x ∘ Cat k con a b
I = Cat k con a c
Cat k con b c
x
  Cat k con b c
x ∘ Cat k con a b
y = Cat k con b c
x Cat k con b c -> Cat k con a b -> Cat k con a c
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 = Cat k con (a ⊗ c) (b, d)
forall (k :: * -> * -> *) (con :: * -> Constraint) a. Cat k con a a
I
  U' Unitor con b a
a × Cat k con c d
I = Unitor con (b, c) (a ⊗ c) -> Cat k con (a ⊗ c) (b, c)
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' (Unitor con b a -> Unitor con (b, c) (a ⊗ c)
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 = Unitor con (a, d) (a ⊗ c) -> Cat k con (a ⊗ c) (a, d)
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' (Unitor con d c -> Unitor con (a, d) (a ⊗ c)
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 Cat k con a b -> Cat k con c d -> Cat k con (a ⊗ c) (b, d)
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 =  Cat k con ((a, b), c) (a, (b, c))
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' = Cat k con (a, (b, c)) ((a, b), c)
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 = Cat k con (a, b) (b, a)
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 = Unitor con a (a, ()) -> Cat k con a (a, ())
forall (con :: * -> Constraint) a b (k :: * -> * -> *).
Unitor con a b -> Cat k con a b
U Unitor con a (a, ())
forall (con :: * -> Constraint) a. Unitor con a (a, ())
UR
  unitor' :: forall a. Obj (Cat k con) a => Cat k con (a ⊗ ()) a
unitor' = Unitor con a (a, ()) -> Cat k con (a, ()) a
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con a (a, ())
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 = ProtoSimplifier k con -> Simplifier k con
forall (k :: * -> * -> *) (con :: * -> Constraint).
ProtoSimplifier k con -> Simplifier k con
mkSimplifier (\Composer k con
x -> Composer k con -> PartialComposer k con
forall (k :: * -> * -> *) (con :: * -> Constraint).
ProtoSimplifier k con
monoidalRules Composer k con
x)

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 -> Maybe (Cat k con a c) -> Alt Maybe (Cat k con a c)
forall {k} (f :: k -> *) (a :: k). f a -> Alt f a
Alt (Cat k con b c -> Cat k con a b -> Maybe (Cat k con a c)
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 = Cat k con a a -> Maybe (Cat k con a a)
forall a. a -> Maybe a
Just Cat k con a a
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 = Cat k con a a -> Maybe (Cat k con a a)
forall a. a -> Maybe a
Just Cat k con a a
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' = Cat k con a a -> Maybe (Cat k con a a)
forall a. a -> Maybe a
Just Cat k con a a
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 = Cat k con a c -> Maybe (Cat k con a c)
forall a. a -> Maybe a
Just (Unitor con c b -> Unitor con a b -> Cat k con a c
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) = Cat k con (a, c) (d ⊗ b) -> Maybe (Cat k con (a, c) (d ⊗ b))
forall a. a -> Maybe a
Just ((Cat k con c d
g Cat k con c d -> Cat k con a b -> Cat k con (c ⊗ a) (d ⊗ 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)
× Cat k con a b
f) Cat k con (c ⊗ a) (d ⊗ b)
-> Cat k con (a, c) (c ⊗ a) -> Cat k con (a, c) (d ⊗ b)
Composer k con
. Cat k con (a, c) (c ⊗ a)
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 = Cat k con ((a ⊗ b) ⊗ c) ((b, c) ⊗ a)
-> Maybe (Cat k con ((a ⊗ b) ⊗ c) ((b, c) ⊗ a))
forall a. a -> Maybe a
Just (Cat k con (b ⊗ (c ⊗ a)) ((b, c) ⊗ 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 con (b ⊗ (c ⊗ a)) ((b, c) ⊗ a)
-> Cat k con (b ⊗ (a ⊗ c)) (b ⊗ (c ⊗ a))
-> Cat k con (b ⊗ (a ⊗ c)) ((b, c) ⊗ a)
Composer k con
. (Cat k con b b
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id Cat k con b b
-> Cat k con (a ⊗ c) (c ⊗ a)
-> Cat k con (b ⊗ (a ⊗ c)) (b ⊗ (c ⊗ 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)
× Cat k con (a ⊗ c) (c ⊗ a)
forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap) Cat k con (b ⊗ (a ⊗ c)) ((b, c) ⊗ a)
-> Cat k con ((b ⊗ a) ⊗ c) (b ⊗ (a ⊗ c))
-> Cat k con ((b ⊗ a) ⊗ c) ((b, c) ⊗ a)
Composer k con
. Cat k con ((b ⊗ a) ⊗ c) (b ⊗ (a ⊗ c))
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 ⊗ a) ⊗ c) ((b, c) ⊗ a)
-> Cat k con ((a ⊗ b) ⊗ c) ((b ⊗ a) ⊗ c)
-> Cat k con ((a ⊗ b) ⊗ c) ((b, c) ⊗ a)
Composer k con
. (Cat k con (a ⊗ b) (b ⊗ a)
forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap Cat k con (a ⊗ b) (b ⊗ a)
-> Cat k con c c -> Cat k con ((a ⊗ b) ⊗ c) ((b ⊗ a) ⊗ c)
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 c
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' = Cat k con (a ⊗ (b ⊗ b)) (b ⊗ (a, b))
-> Maybe (Cat k con (a ⊗ (b ⊗ b)) (b ⊗ (a, b)))
forall a. a -> Maybe a
Just (Cat k con ((b ⊗ a) ⊗ b) (b ⊗ (a, b))
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 ⊗ a) ⊗ b) (b ⊗ (a, b))
-> Cat k con ((a ⊗ b) ⊗ b) ((b ⊗ a) ⊗ b)
-> Cat k con ((a ⊗ b) ⊗ b) (b ⊗ (a, b))
Composer k con
. (Cat k con (a ⊗ b) (b ⊗ a)
forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap Cat k con (a ⊗ b) (b ⊗ a)
-> Cat k con b b -> Cat k con ((a ⊗ b) ⊗ b) ((b ⊗ a) ⊗ 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)
× Cat k con b b
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id) Cat k con ((a ⊗ b) ⊗ b) (b ⊗ (a, b))
-> Cat k con (a ⊗ (b ⊗ b)) ((a ⊗ b) ⊗ b)
-> Cat k con (a ⊗ (b ⊗ b)) (b ⊗ (a, b))
Composer k con
. Cat k con (a ⊗ (b ⊗ b)) ((a ⊗ b) ⊗ b)
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 (a ⊗ (b ⊗ b)) (b ⊗ (a, b))
-> Cat k con (a ⊗ (b ⊗ b)) (a ⊗ (b ⊗ b))
-> Cat k con (a ⊗ (b ⊗ b)) (b ⊗ (a, b))
Composer k con
. (Cat k con a a
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id Cat k con a a
-> Cat k con (b ⊗ b) (b ⊗ b)
-> Cat k con (a ⊗ (b ⊗ b)) (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)
× Cat k con (b ⊗ b) (b ⊗ b)
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 = Cat k con (c ⊗ (a, b)) (a, (b, c))
-> Maybe (Cat k con (c ⊗ (a, b)) (a, (b, c)))
forall a. a -> Maybe a
Just ((Cat k con a a
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id Cat k con a a
-> Cat k con (c ⊗ b) (b, c) -> Cat k con (a ⊗ (c ⊗ b)) (a, (b, c))
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 ⊗ b) (b, c)
forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap) Cat k con (a ⊗ (c ⊗ b)) (a, (b, c))
-> Cat k con ((a ⊗ c) ⊗ b) (a ⊗ (c ⊗ b))
-> Cat k con ((a ⊗ c) ⊗ b) (a, (b, c))
Composer k con
. Cat k con ((a ⊗ c) ⊗ b) (a ⊗ (c ⊗ b))
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 ((a ⊗ c) ⊗ b) (a, (b, c))
-> Cat k con ((c ⊗ a) ⊗ b) ((a ⊗ c) ⊗ b)
-> Cat k con ((c ⊗ a) ⊗ b) (a, (b, c))
Composer k con
. (Cat k con (c ⊗ a) (a ⊗ c)
forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap Cat k con (c ⊗ a) (a ⊗ c)
-> Cat k con b b -> Cat k con ((c ⊗ a) ⊗ b) ((a ⊗ c) ⊗ 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)
× Cat k con b b
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id) Cat k con ((c ⊗ a) ⊗ b) (a, (b, c))
-> Cat k con (c ⊗ (a, b)) ((c ⊗ a) ⊗ b)
-> Cat k con (c ⊗ (a, b)) (a, (b, c))
Composer k con
. Cat k con (c ⊗ (a, b)) ((c ⊗ a) ⊗ b)
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 = Cat k con ((b, c) ⊗ a) ((a, b), c)
-> Maybe (Cat k con ((b, c) ⊗ a) ((a, b), c))
forall a. a -> Maybe a
Just ((Cat k con (b ⊗ a) (a, b)
forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap Cat k con (b ⊗ a) (a, b)
-> Cat k con c c -> Cat k con ((b ⊗ a) ⊗ c) ((a, b), c)
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 c
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id) Cat k con ((b ⊗ a) ⊗ c) ((a, b), c)
-> Cat k con (b ⊗ (a ⊗ c)) ((b ⊗ a) ⊗ c)
-> Cat k con (b ⊗ (a ⊗ c)) ((a, b), c)
Composer k con
. Cat k con (b ⊗ (a ⊗ c)) ((b ⊗ a) ⊗ c)
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 ⊗ (a ⊗ c)) ((a, b), c)
-> Cat k con (b ⊗ (c ⊗ a)) (b ⊗ (a ⊗ c))
-> Cat k con (b ⊗ (c ⊗ a)) ((a, b), c)
Composer k con
. (Cat k con b b
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id Cat k con b b
-> Cat k con (c ⊗ a) (a ⊗ c)
-> Cat k con (b ⊗ (c ⊗ a)) (b ⊗ (a ⊗ c))
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 ⊗ a) (a ⊗ c)
forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap ) Cat k con (b ⊗ (c ⊗ a)) ((a, b), c)
-> Cat k con ((b, c) ⊗ a) (b ⊗ (c ⊗ a))
-> Cat k con ((b, c) ⊗ a) ((a, b), c)
Composer k con
. Cat k con ((b, c) ⊗ a) (b ⊗ (c ⊗ 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)

  -- push U' through S
  U' Unitor con c b
UR `after` Cat k con a b
S = Cat k con ((), c) c -> Maybe (Cat k con ((), c) c)
forall a. a -> Maybe a
Just (Unitor con c ((), c) -> Cat k con ((), c) c
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con c ((), c)
forall (con :: * -> Constraint) a. Unitor con a ((), a)
UL)
  U' Unitor con c b
UL `after` Cat k con a b
S = Cat k con (c, ()) c -> Maybe (Cat k con (c, ()) c)
forall a. a -> Maybe a
Just (Unitor con c (c, ()) -> Cat k con (c, ()) c
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con c (c, ())
forall (con :: * -> Constraint) a. Unitor con a (a, ())
UR)
  U' (IL Unitor con a b
a) `after` Cat k con a b
S = Cat k con (c, b) (a, c) -> Maybe (Cat k con (c, b) (a, c))
forall a. a -> Maybe a
Just (Cat k con (c ⊗ a) (a, c)
forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap Cat k con (c ⊗ a) (a, c)
-> Cat k con (c, b) (c ⊗ a) -> Cat k con (c, b) (a, c)
Composer k con
. Unitor con (c ⊗ a) (c, b) -> Cat k con (c, b) (c ⊗ a)
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' (Unitor con a b -> Unitor con (c ⊗ a) (c, b)
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 = Cat k con (b, c) (c, a) -> Maybe (Cat k con (b, c) (c, a))
forall a. a -> Maybe a
Just (Cat k con (a ⊗ c) (c, a)
forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap Cat k con (a ⊗ c) (c, a)
-> Cat k con (b, c) (a ⊗ c) -> Cat k con (b, c) (c, a)
Composer k con
. Unitor con (a ⊗ c) (b, c) -> Cat k con (b, c) (a ⊗ c)
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' (Unitor con a b -> Unitor con (a ⊗ c) (b, c)
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) = Cat k con a b -> Maybe (Cat k con a b)
forall a. a -> Maybe a
Just (Cat k con a b
f Cat k con a b -> Cat k con (a, ()) a -> Cat k con (a, ()) b
Composer k con
. Unitor con a (a, ()) -> Cat k con (a, ()) a
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con a (a, ())
forall (con :: * -> Constraint) a. Unitor con a (a, ())
UR  Cat k con (a, ()) b -> Cat k con a (a, ()) -> Cat k con a b
Composer k con
. Cat k con a b
Cat k con a (a, ())
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) = Cat k con a (a ⊗ d) -> Maybe (Cat k con a (a ⊗ d))
forall a. a -> Maybe a
Just (((Unitor con a b -> Cat k con b a
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con a b
a Cat k con b a -> Cat k con a b -> Cat k con a a
Composer k con
. Cat k con a b
Cat k con a b
f) Cat k con a a -> Cat k con c d -> Cat k con (a, c) (a ⊗ d)
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)  Cat k con (a, c) (a ⊗ d)
-> Cat k con a (a, c) -> Cat k con a (a ⊗ d)
Composer k con
. Cat k con a b
Cat k con a (a, c)
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) = Cat k con a (b ⊗ a) -> Maybe (Cat k con a (b ⊗ a))
forall a. a -> Maybe a
Just ((Cat k con a b
f Cat k con a b -> Cat k con c a -> Cat k con (a, c) (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)
× (Unitor con a b -> Cat k con b a
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con a b
a Cat k con b a -> Cat k con c b -> Cat k con c a
Composer k con
. Cat k con c b
Cat k con c d
g))  Cat k con (a, c) (b ⊗ a)
-> Cat k con a (a, c) -> Cat k con a (b ⊗ a)
Composer k con
. Cat k con a b
Cat k con a (a, c)
h )

  -- push U' through A'
  U' Unitor con c b
UR `after` Cat k con a b
A' = Cat k con (a ⊗ (b, ())) (a, b)
-> Maybe (Cat k con (a ⊗ (b, ())) (a, b))
forall a. a -> Maybe a
Just (Cat k con a a
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id Cat k con a a
-> Cat k con (b, ()) b -> Cat k con (a ⊗ (b, ())) (a, 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)
× Unitor con b (b, ()) -> Cat k con (b, ()) b
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con b (b, ())
forall (con :: * -> Constraint) a. Unitor con a (a, ())
UR)
  U' (IR Unitor con a b
a) `after` Cat k con a b
A' = Cat k con (a ⊗ (b ⊗ b)) ((a, b), a)
-> Maybe (Cat k con (a ⊗ (b ⊗ b)) ((a, b), a))
forall a. a -> Maybe a
Just (Cat k con (a, (b, a)) ((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)) ((a, b), a)
-> Cat k con (a ⊗ (b ⊗ b)) (a, (b, a))
-> Cat k con (a ⊗ (b ⊗ b)) ((a, b), a)
Composer k con
. (Cat k con a a
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id Cat k con a a
-> Cat k con (b ⊗ b) (b, a) -> Cat k con (a ⊗ (b ⊗ b)) (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)
× (Cat k con b b
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id Cat k con b b -> Cat k con b a -> Cat k con (b ⊗ b) (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)
× Unitor con a b -> Cat k con b a
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' = Cat k con (c ⊗ (b ⊗ c)) ((c, a), c)
-> Maybe (Cat k con (c ⊗ (b ⊗ c)) ((c, a), c))
forall a. a -> Maybe a
Just (Cat k con (c, (a, c)) ((c, a), c)
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 (c, (a, c)) ((c, a), c)
-> Cat k con (c ⊗ (b ⊗ c)) (c, (a, c))
-> Cat k con (c ⊗ (b ⊗ c)) ((c, a), c)
Composer k con
. (Cat k con c c
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id Cat k con c c
-> Cat k con (b ⊗ c) (a, c) -> Cat k con (c ⊗ (b ⊗ c)) (c, (a, c))
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)
× (Unitor con a b -> Cat k con b a
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con a b
a Cat k con b a -> Cat k con c c -> Cat k con (b ⊗ c) (a, c)
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 c
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' = Cat k con (a ⊗ ((), c)) (a, c)
-> Maybe (Cat k con (a ⊗ ((), c)) (a, c))
forall a. a -> Maybe a
Just (Cat k con a a
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id Cat k con a a
-> Cat k con ((), c) c -> Cat k con (a ⊗ ((), c)) (a, c)
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)
× Unitor con c ((), c) -> Cat k con ((), c) c
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con c ((), c)
forall (con :: * -> Constraint) a. Unitor con a ((), a)
UL )
  U' (IL Unitor con a b
UL)     `after` Cat k con a b
A' = Cat k con ((), c) c -> Maybe (Cat k con ((), c) c)
forall a. a -> Maybe a
Just (Unitor con c ((), c) -> Cat k con ((), c) c
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con c ((), c)
forall (con :: * -> Constraint) a. Unitor con a ((), a)
UL)
  U' (IL (IL Unitor con a b
a)) `after` Cat k con a b
A' = Cat k con (b ⊗ (c, c)) ((a, c), c)
-> Maybe (Cat k con (b ⊗ (c, c)) ((a, c), c))
forall a. a -> Maybe a
Just (Cat k con (a, (c, c)) ((a, c), c)
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, (c, c)) ((a, c), c)
-> Cat k con (b ⊗ (c, c)) (a, (c, c))
-> Cat k con (b ⊗ (c, c)) ((a, c), c)
Composer k con
. (Unitor con a b -> Cat k con b a
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con a b
a Cat k con b a
-> Cat k con (c, c) (c, c) -> Cat k con (b ⊗ (c, c)) (a, (c, c))
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, c) (c, c)
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 = Cat k con (((), b) ⊗ c) (b, c)
-> Maybe (Cat k con (((), b) ⊗ c) (b, c))
forall a. a -> Maybe a
Just (Unitor con b ((), b) -> Cat k con ((), b) b
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con b ((), b)
forall (con :: * -> Constraint) a. Unitor con a ((), a)
UL Cat k con ((), b) b
-> Cat k con c c -> Cat k con (((), b) ⊗ c) (b, c)
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 c
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 = Cat k con ((b ⊗ b) ⊗ c) (a, (b, c))
-> Maybe (Cat k con ((b ⊗ b) ⊗ c) (a, (b, c)))
forall a. a -> Maybe a
Just (Cat k con ((a, b), c) (a, (b, c))
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), c) (a, (b, c))
-> Cat k con ((b ⊗ b) ⊗ c) ((a, b), c)
-> Cat k con ((b ⊗ b) ⊗ c) (a, (b, c))
Composer k con
. ((Unitor con a b -> Cat k con b a
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con a b
a Cat k con b a -> Cat k con b b -> Cat k con (b ⊗ b) (a, 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)
× Cat k con b b
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id) Cat k con (b ⊗ b) (a, b)
-> Cat k con c c -> Cat k con ((b ⊗ b) ⊗ c) ((a, b), c)
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 c
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 = Cat k con ((c ⊗ b) ⊗ c) (c, (a, c))
-> Maybe (Cat k con ((c ⊗ b) ⊗ c) (c, (a, c)))
forall a. a -> Maybe a
Just (Cat k con ((c, a), c) (c, (a, c))
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 ((c, a), c) (c, (a, c))
-> Cat k con ((c ⊗ b) ⊗ c) ((c, a), c)
-> Cat k con ((c ⊗ b) ⊗ c) (c, (a, c))
Composer k con
. ((Cat k con c c
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id Cat k con c c -> Cat k con b a -> Cat k con (c ⊗ b) (c, 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)
× Unitor con a b -> Cat k con b a
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con a b
a) Cat k con (c ⊗ b) (c, a)
-> Cat k con c c -> Cat k con ((c ⊗ b) ⊗ c) ((c, a), c)
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 c
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 = Cat k con ((c, ()) ⊗ a) (c, a)
-> Maybe (Cat k con ((c, ()) ⊗ a) (c, a))
forall a. a -> Maybe a
Just (Unitor con c (c, ()) -> Cat k con (c, ()) c
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con c (c, ())
forall (con :: * -> Constraint) a. Unitor con a (a, ())
UR Cat k con (c, ()) c
-> Cat k con a a -> Cat k con ((c, ()) ⊗ a) (c, 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)
× Cat k con a a
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 = Cat k con (c, ()) c -> Maybe (Cat k con (c, ()) c)
forall a. a -> Maybe a
Just (Unitor con c (c, ()) -> Cat k con (c, ()) c
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con c (c, ())
forall (con :: * -> Constraint) a. Unitor con a (a, ())
UR)
  U' (IR (IR Unitor con a b
a)) `after` Cat k con a b
A = Cat k con ((c, c) ⊗ b) (c, (c, a))
-> Maybe (Cat k con ((c, c) ⊗ b) (c, (c, a)))
forall a. a -> Maybe a
Just (Cat k con ((c, c), a) (c, (c, 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 ((c, c), a) (c, (c, a))
-> Cat k con ((c, c) ⊗ b) ((c, c), a)
-> Cat k con ((c, c) ⊗ b) (c, (c, a))
Composer k con
. (Cat k con (c, c) (c, c)
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id Cat k con (c, c) (c, c)
-> Cat k con b a -> Cat k con ((c, c) ⊗ b) ((c, c), 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)
× Unitor con a b -> Cat k con b a
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) = Cat k con (a, c) (b, d) -> Maybe (Cat k con (a, c) (b, d))
forall a. a -> Maybe a
Just ((Cat k con a b
f Cat k con a b -> Cat k con a a -> Cat k con a b
Composer k con
. Cat k con a a
Cat k con a b
h) Cat k con a b -> Cat k con c d -> Cat k con (a, c) (b, d)
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 Cat k con c d -> Cat k con c c -> Cat k con c d
Composer k con
. Cat k con c c
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 = Cat k con a (b, d) -> Maybe (Cat k con a (b, d))
forall a. a -> Maybe a
Just ((Cat k con b b
fCat k con b b -> Cat k con c d -> Cat k con (b ⊗ c) (b, d)
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) Cat k con (b ⊗ c) (b, d)
-> Cat k con (a, c) (b ⊗ c) -> Cat k con (a, c) (b, d)
Composer k con
. Unitor con (b ⊗ c) (a, c) -> Cat k con (a, c) (b ⊗ c)
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' (Unitor con b a -> Unitor con (b ⊗ c) (a, c)
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, c) (b, d) -> Cat k con a (a, c) -> Cat k con a (b, d)
Composer k con
. Cat k con a b
Cat k con a (a, c)
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 = Cat k con a (b, d) -> Maybe (Cat k con a (b, d))
forall a. a -> Maybe a
Just ((Cat k con a b
f Cat k con a b -> Cat k con b d -> Cat k con (a ⊗ b) (b, d)
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) Cat k con (a ⊗ b) (b, d)
-> Cat k con (a, c) (a ⊗ b) -> Cat k con (a, c) (b, d)
Composer k con
. Unitor con (a ⊗ b) (a, c) -> Cat k con (a, c) (a ⊗ b)
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' (Unitor con b c -> Unitor con (a ⊗ b) (a, c)
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) Cat k con (a, c) (b, d) -> Cat k con a (a, c) -> Cat k con a (b, d)
Composer k con
. Cat k con a b
Cat k con a (a, c)
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) = Cat k con (a, c) c -> Maybe (Cat k con (a, c) c)
forall a. a -> Maybe a
Just (Cat k con b c
h Cat k con b c -> Cat k con (b ⊗ c) b -> Cat k con (b ⊗ c) c
Composer k con
. (Cat k con b b
f Cat k con b b -> Cat k con c d -> Cat k con (b ⊗ c) (b, d)
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) Cat k con (b ⊗ c) c
-> Cat k con (a, c) (b ⊗ c) -> Cat k con (a, c) c
Composer k con
. Unitor con (b ⊗ c) (a, c) -> Cat k con (a, c) (b ⊗ c)
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' (Unitor con b a -> Unitor con (b ⊗ c) (a, c)
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)) = Cat k con (a, c) c -> Maybe (Cat k con (a, c) c)
forall a. a -> Maybe a
Just (Cat k con b c
h Cat k con b c -> Cat k con (a ⊗ b) b -> Cat k con (a ⊗ b) c
Composer k con
. (Cat k con a b
f Cat k con a b -> Cat k con b d -> Cat k con (a ⊗ b) (b, d)
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) Cat k con (a ⊗ b) c
-> Cat k con (a, c) (a ⊗ b) -> Cat k con (a, c) c
Composer k con
. Unitor con (a ⊗ b) (a, c) -> Cat k con (a, c) (a ⊗ b)
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' (Unitor con b c -> Unitor con (a ⊗ b) (a, c)
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
_ = Maybe (Cat k con a c)
forall a. Maybe a
Nothing


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




{-

closedCartesianRules :: forall k con. ProtoSimplifier k con
closedCartesianRules (.) = \ x y -> Alt (after x 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)
  
  -- Incomplete support for apply/curry simplifier
  Apply `after` (Curry f :×: I) = Just f
  -- Apply `after` (Curry (g :>: R) :▵: f) = Just (g . f)
  _ `after` _ = 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 = Cat k con a b -> Cat k con a b
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
Cat k con a c
g -- g is already normal.
   Cat k con b c
f ... Cat k con a b
I  = Cat k con a c
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 Alt Maybe (Cat k con b b) -> Maybe (Cat k con b b)
forall {k} (f :: k -> *) (a :: k). Alt f a -> f a
getAlt (Cat k con b b
g Cat k con b b -> Cat k con b b -> Alt Maybe (Cat k con b b)
PartialComposer k con
`after` Cat k con b b
h) of
     Maybe (Cat k con b b)
Nothing -> (Cat k con b c
f Cat k con b c -> Cat k con b b -> Cat k con b c
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) Cat k con b c -> Cat k con a b -> Cat k con a c
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 Cat k con b b -> Cat k con a b -> Cat k con a 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
:<: 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 Cat k con b c -> Cat k con b b -> Cat k con b c
Composer k con
... Cat k con b b
j Cat k con b c -> Cat k con a b -> Cat k con a c
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 Cat k con b c -> Cat k con a b -> Cat k con a c
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
Composer k con -> PartialComposer 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) = Cat k con a b -> Cat k con a b
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 a b -> Cat k con c d -> Cat k con (a, c) (b, d)
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 -> Cat k con c 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) = Cat k con b b -> Cat k con b b
forall a b. (con a, con b) => Cat k con a b -> Cat k con a b
simplify Cat k con b b
f Cat k con b b -> Cat k con a b -> Cat k con a b
Composer k con
... Cat k con a b -> Cat k con a b
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 -> Cat k con a b
forall (k :: * -> * -> *) (con :: * -> Constraint) a. Cat k con a a
I
  (Cat k con a b
f :×: Cat k con c d
g) -> Cat k con a b -> Cat k con a b
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 Cat k con a b -> Cat k con c d -> Cat k con (a, c) (b, d)
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 -> Cat k con c 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) -> Cat k con b b -> Cat k con b b
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 Cat k con b b -> Cat k con a b -> Cat k con a b
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. Cat k con a b -> Cat k con a b
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
ϕ -> k a b -> Cat k con 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 -> Cat k con a b
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' -> Cat k con a b
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 -> Cat k con a b
forall (con :: * -> Constraint) a b (k :: * -> * -> *).
(con a, con b) =>
Cat k con (a, b) (b, a)
S
  (U Unitor con a b
u) -> Unitor con a b -> Cat k con a b
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) -> Unitor con b a -> Cat k con a b
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 -> Cat k con a b
forall (k :: * -> * -> *) (con :: * -> Constraint) a. Cat k con a a
I
  (Cat k con a b
f :×: Cat k con c d
g) -> Cat k con a b -> Cat k con a b
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 Cat k con a b -> Cat k con c d -> Cat k con (a, c) (b, d)
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 -> Cat k con c 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) -> Cat k con b b -> Cat k con b b
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 Cat k con b b -> Cat k con a b -> Cat k con a b
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. Cat k con a b -> Cat k con a b
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
ϕ -> k a b -> Cat k con 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 -> Cat k con a b
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' -> Cat k con a b
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 -> Cat k con a b
forall (con :: * -> Constraint) a b (k :: * -> * -> *).
(con a, con b) =>
Cat k con (a, b) (b, a)
S
  (U Unitor con a b
u) -> Unitor con a b -> Cat k con a b
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) -> Unitor con b a -> Cat k con a b
forall (con :: * -> Constraint) b a (k :: * -> * -> *).
Unitor con b a -> Cat k con a b
U' Unitor con b a
u