module Monocle where

import Monocle.Core
import Monocle.Markup
import Monocle.Tex

obA = object "A"
obB = object "B"
obC = object "C"
obD = object "D"


-- Duality:

ldual'of x = Func "ldual" [x] Function
ldual x = ldual'of x
ldual'r x = ldual'of x

rdual'of x = Func "rdual" [x] Function
rdual x = rdual'of x
rdual'r x = rdual'of x

unit'of nm x y = if (x == ldual y) || (y == rdual x)
    then let f = (element nm (y \* x)) in Transform "unit" f [x, y]
    else error "unit'of: not a dual pair"
unit x y = unit'of "\\eta" x y
unit'r x y = let f = (element "*\\eta" (y \* x)) in Transform "unit" f [x, y]

counit'of nm x y = if (x == ldual y) || (y == rdual x)
    then let f = (coelement nm (x \* y)) in Transform "counit" f [x, y]
    else error "counit'of: not a dual pair"
counit x y = counit'of "\\epsilon" x y
counit'r x y = let f = (coelement "*\\epsilon" (x \* y)) in Transform "counit" f [x, y]

zigzag'rule'Left = (counit'r obA obB) \* obA \. obA \* (unit'r obA obB) \== obA
zigzag'rule'Right =  obB \* (counit'r obA obB) \. (unit'r obA obB) \* obB \== obB

-- Braiding:

braid'of nm x y = let f = (arrow nm (x \* y) (y \* x)) in
    Transform "braid" f [x, y]
braid x y = braid'of "\\beta" x y
braid'r x y = braid'of ("*\\beta") x y

unbraid'of nm x y = let f = (arrow nm (x \* y) (y \* x)) in
    Transform "unbraid" f [x, y]
unbraid x y = unbraid'of "\\beta^{-1}" x y
unbraid'r x y = unbraid'of ("*\\beta^{-1}") x y

braid'rule'Iso'Left = (unbraid'r obB obA) \. (braid'r obA obB) \== obA \* obB

braid'rule'Iso'Right = (braid'r obB obA) \. (unbraid'r obA obB) \== obA \* obB

braid'rule'Nat'Left = let f = arrow "f" obA obA in
     (braid'r obA obB) \. f \* obB \== obB \* f \. (braid'r obA obB)

braid'rule'Nat'Right = let f = arrow "f" obB obB in
     (braid'r obA obB) \. obA \* f \== f \* obA \. (braid'r obA obB)

braid'rule'Hex'Braid =
    obB \* (braid'r obA obC) \. (braid'r obA obB) \* obC \== braid'r obA (obB \* obC)

braid'rule'Hex'Unbraid =
    obB \* (unbraid'r obA obC) \. (unbraid'r obA obB) \* obC \== unbraid'r obA (obB \* obC)

-- Symmetry:

cross'rule = braid'r obA obB \== unbraid'r obA obB

-- Twisting:

twist'of nm x = let f = (arrow nm x x) in Transform "twist" f [x]
twist x = twist'of "\\theta" x
twist'r x = twist'of ("*\\theta") x

untwist'of nm x = let f = (arrow nm x x) in Transform "untwist" f [x]
untwist x = untwist'of "\\theta^{-1}" x
untwist'r x = untwist'of ("*\\theta^{-1}") x

untwist'rule'Iso'Left = (untwist'r obA) \. (twist'r obA) \== obA \* obB
untwist'rule'Iso'Right = (twist'r obA) \. (untwist'r obA) \== obA

twist'rule'Id = (twist'r tid) \== tid

twist'rule'Natural = let f = arrow "f" obA obA in
    (twist'r obA) \. f \== f \. (twist'r obA)

twist'rule'Braid =
    (braid'r obB obA) \. (twist'r obB) \* (twist'r obA) \. (braid'r obA obB) \== twist'r (obA \* obB)

-- Dagger:

dagger'of f = Func "dagger" [f] Cofunctor

dagger f = dagger'of f
dagger'r f = dagger'of f

dagger'rule'Id = (dagger'r obA) \== obA
dagger'rule'Cofunctor = let f = arrow "f" obB obC; g = arrow "g" obA obB in
    (dagger'r (f \. g)) \== (dagger'r g) \. (dagger'r f)
dagger'rule'Inv = (dagger'r $ dagger'r obA) \== obA