module Monocle.Rules where

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

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


-- * Duality

-- | For given object create it's left dual: <http://en.wikipedia.org/wiki/Dual_object>.
ldual'of :: Mor a -> Mor a
ldual'of x = Func "ldual" [x] Function

-- | Same as 'ldual'of', for usage in calculations.
ldual :: Mor a -> Mor a
ldual x = ldual'of x

-- | Same as 'ldual'of', for usage in rule descriptions.
ldual'r :: Mor a -> Mor a
ldual'r x = ldual'of x

-- | For given object create it's right dual: <http://en.wikipedia.org/wiki/Dual_object>.
rdual'of :: Mor a -> Mor a
rdual'of x = Func "rdual" [x] Function

-- | Same as 'rdual'of', for usage in calculations.
rdual :: Mor a -> Mor a
rdual x = rdual'of x

-- | Same as 'rdual'of', for usage in rule descriptions.
rdual'r :: Mor a -> Mor a
rdual'r x = rdual'of x

-- | For given dual pair of objects @(x, y)@ and name @nm@ call @unit'of nm x y@ to create named
-- duality unit arrow. Generates error if @(x, y)@ is not a dual pair.
unit'of :: (Eq a) => a -> Mor a -> Mor a -> Mor a
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"

-- | Same as @'unit'of' \"\\\\eta\"@, for usage in calculations.
unit :: Mor String -> Mor String -> Mor String
unit = unit'of "\\eta"

-- | Same as @'unit'of' \"*\\\\eta\"@, except that it does not check duality. For usage in
-- rule descriptions.
unit'r :: Mor String -> Mor String -> Mor String
unit'r x y = let f = (element "*\\eta" (y \* x)) in Transform "unit" f [x, y]

-- | For given dual pair of objects @(x, y)@ and name @nm@ call @counit'of nm x y@ to create named
-- duality counit arrow. Generates error if @(x, y)@ is not a dual pair.
counit'of :: (Eq a) => a -> Mor a -> Mor a -> Mor a
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"

-- | Same as @'counit'of' \"\\\\epsilon\"@, for usage in calculations.
counit :: Mor String -> Mor String -> Mor String
counit = counit'of "\\epsilon"

-- | Same as @'counit'of' \"*\\\\epsilon\"@, except that it does not check duality. For usage in
-- rule descriptions.
counit'r :: Mor String -> Mor String -> Mor String
counit'r x y = let f = (coelement "*\\epsilon" (x \* y)) in Transform "counit" f [x, y]

-- | One of \"zigzag rules\" for duality.
zigzag'rule'Left :: Rule String
zigzag'rule'Left = (counit'r obA obB) \* obA \. obA \* (unit'r obA obB) \== obA

-- | One of \"zigzag rules\" for duality.
zigzag'rule'Right :: Rule String
zigzag'rule'Right =  obB \* (counit'r obA obB) \. (unit'r obA obB) \* obB \== obB

-- * Braiding

-- | For given pair of objects @(x, y)@ and name @nm@ call @braid'of nm x y@ to create named
-- braid arrow: <http://en.wikipedia.org/wiki/Braided_monoidal_category>
braid'of :: (Eq a) => a -> Mor a -> Mor a -> Mor a
braid'of nm x y = let f = (arrow nm (x \* y) (y \* x)) in
    Transform "braid" f [x, y]

-- | Same as @'braid'of' \"\\\\beta\"@, for usage in calculations.
braid :: Mor String -> Mor String -> Mor String
braid x y = braid'of "\\beta" x y

-- | Same as @'braid'of' \"*\\\\beta\"@, for usage in rule descriptions.
braid'r :: Mor String -> Mor String -> Mor String
braid'r x y = braid'of ("*\\beta") x y

-- | For given pair of objects @(x, y)@ and name @nm@ call @unbraid'of nm x y@ to create named
-- unbraid arrow (inverse of braid arrow).
unbraid'of :: (Eq a) => a -> Mor a -> Mor a -> Mor a
unbraid'of nm x y = let f = (arrow nm (x \* y) (y \* x)) in
    Transform "unbraid" f [x, y]

-- | Same as @'unbraid'of' \"\\\\beta^{-1}\"@, for usage in calculations.
unbraid :: Mor String -> Mor String -> Mor String
unbraid x y = unbraid'of "\\beta^{-1}" x y

-- | Same as @'unbraid'of' \"*\\\\beta^{-1}\"@, for usage in rule descriptions.
unbraid'r :: Mor String -> Mor String -> Mor String
unbraid'r x y = unbraid'of ("*\\beta^{-1}") x y

-- | Isomorphism rule: 'unbraid' as inverse of 'braid'.
braid'rule'Iso'Left :: Rule String
braid'rule'Iso'Left = (unbraid'r obB obA) \. (braid'r obA obB) \== obA \* obB

-- | Isomorphism rule: 'braid' as inverse of 'unbraid'.
braid'rule'Iso'Right :: Rule String
braid'rule'Iso'Right = (braid'r obB obA) \. (unbraid'r obA obB) \== obA \* obB

-- | Naturality rule on the \"left wire\".
braid'rule'Nat'Left :: Rule String
braid'rule'Nat'Left = let f = arrow "f" obA obA in
     (braid'r obA obB) \. f \* obB \== obB \* f \. (braid'r obA obB)

-- | Naturality rule on the \"right wire\".
braid'rule'Nat'Right :: Rule String
braid'rule'Nat'Right = let f = arrow "f" obB obB in
     (braid'r obA obB) \. obA \* f \== f \* obA \. (braid'r obA obB)

-- | Hexagon identity for 'braid', strict monoidal case.
braid'rule'Hex'Braid :: Rule String
braid'rule'Hex'Braid =
    obB \* (braid'r obA obC) \. (braid'r obA obB) \* obC \== braid'r obA (obB \* obC)

-- | Hexagon identity for 'unbraid', strict monoidal case.
braid'rule'Hex'Unbraid :: Rule String
braid'rule'Hex'Unbraid =
    obB \* (unbraid'r obA obC) \. (unbraid'r obA obB) \* obC \== unbraid'r obA (obB \* obC)

-- * Symmetry

-- | Rule for the \"cross\" arrow: it's simply self-inverse braid.
cross'rule :: Rule String
cross'rule = braid'r obA obB \== unbraid'r obA obB

-- * Twisting

-- | For given object @x@ and name @nm@ call @twist'of nm x@ to create named
-- twist arrow.
twist'of :: (Eq a) => a -> Mor a -> Mor a
twist'of nm x = let f = (arrow nm x x) in Transform "twist" f [x]

-- | Same as @'twist'of' \"\\\\theta\"@, for usage in calculations.
twist :: Mor String -> Mor String
twist x = twist'of "\\theta" x

-- | Same as @'twist'of' \"*\\\\theta\"@, for usage in rule descriptions.
twist'r :: Mor String -> Mor String
twist'r x = twist'of ("*\\theta") x

-- | For given object @x@ and name @nm@ call @untwist'of nm x@ to create named
-- untwist arrow.
untwist'of :: (Eq a) => a -> Mor a -> Mor a
untwist'of nm x = let f = (arrow nm x x) in Transform "untwist" f [x]

-- | Same as @'untwist'of' \"\\\\theta^{-1}\"@, for usage in calculations.
untwist :: Mor String -> Mor String
untwist x = untwist'of "\\theta^{-1}" x

-- | Same as @'untwist'of' \"*\\\\theta^{-1}\"@, for usage in rule descriptions.
untwist'r :: Mor String -> Mor String
untwist'r x = untwist'of ("*\\theta^{-1}") x

-- | Isomorphism rule: 'untwist' as inverse of 'twist'.
twist'rule'Iso'Left :: Rule String
twist'rule'Iso'Left = (untwist'r obA) \. (twist'r obA) \== obA \* obB

-- | Isomorphism rule: 'twist' as inverse of 'untwist'.
twist'rule'Iso'Right :: Rule String
twist'rule'Iso'Right = (twist'r obA) \. (untwist'r obA) \== obA

-- | Twisting the identity object changes nothing.
twist'rule'Id :: Rule String
twist'rule'Id = (twist'r tid) \== tid

-- | Twisting naturality.
twist'rule'Natural :: Rule String
twist'rule'Natural = let f = arrow "f" obA obA in
    (twist'r obA) \. f \== f \. (twist'r obA)

-- | Twist\/braid interaction.
twist'rule'Braid :: Rule String
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@ creates daggered version of the arrow @f@.
dagger'of :: (Eq a) => Mor a -> Mor a
dagger'of f = Func "dagger" [f] Cofunctor

-- | Same as 'dagger'of', for usage in calculations.
dagger :: (Eq a) => Mor a -> Mor a
dagger = dagger'of

-- | Same as 'dagger'of', for usage in rule descriptions.
dagger'r :: (Eq a) => Mor a -> Mor a
dagger'r f = dagger'of f

-- | As contravariant functor 'dagger' maps id's to id's.
dagger'rule'Id :: Rule String
dagger'rule'Id = (dagger'r obA) \== obA

-- | 'dagger' is contravariant functor, i.e. inverts composition order.
dagger'rule'Cofunctor :: Rule String
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' involution rule.
dagger'rule'Inv :: Rule String
dagger'rule'Inv = let f = arrow "f" obA obA in (dagger'r $ dagger'r f) \== f