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"
ldual'of :: Mor a -> Mor a
ldual'of x = Func "ldual" [x] Function
ldual :: Mor a -> Mor a
ldual x = ldual'of x
ldual'r :: Mor a -> Mor a
ldual'r x = ldual'of x
rdual'of :: Mor a -> Mor a
rdual'of x = Func "rdual" [x] Function
rdual :: Mor a -> Mor a
rdual x = rdual'of x
rdual'r :: Mor a -> Mor a
rdual'r x = rdual'of x
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"
unit :: Mor String -> Mor String -> Mor String
unit = unit'of "\\eta"
unit'r :: Mor String -> Mor String -> Mor String
unit'r x y = let f = (element "*\\eta" (y \* x)) in Transform "unit" f [x, y]
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"
counit :: Mor String -> Mor String -> Mor String
counit = counit'of "\\epsilon"
counit'r :: Mor String -> Mor String -> Mor String
counit'r x y = let f = (coelement "*\\epsilon" (x \* y)) in Transform "counit" f [x, y]
zigzag'rule'Left :: Rule String
zigzag'rule'Left = (counit'r obA obB) \* obA \. obA \* (unit'r obA obB) \== obA
zigzag'rule'Right :: Rule String
zigzag'rule'Right = obB \* (counit'r obA obB) \. (unit'r obA obB) \* obB \== obB
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]
braid :: Mor String -> Mor String -> Mor String
braid x y = braid'of "\\beta" x y
braid'r :: Mor String -> Mor String -> Mor String
braid'r x y = braid'of ("*\\beta") x y
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]
unbraid :: Mor String -> Mor String -> Mor String
unbraid x y = unbraid'of "\\beta^{-1}" x y
unbraid'r :: Mor String -> Mor String -> Mor String
unbraid'r x y = unbraid'of ("*\\beta^{-1}") x y
braid'rule'Iso'Left :: Rule String
braid'rule'Iso'Left = (unbraid'r obB obA) \. (braid'r obA obB) \== obA \* obB
braid'rule'Iso'Right :: Rule String
braid'rule'Iso'Right = (braid'r obB obA) \. (unbraid'r obA obB) \== obA \* obB
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)
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)
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)
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)
cross'rule :: Rule String
cross'rule = braid'r obA obB \== unbraid'r obA obB
twist'of :: (Eq a) => a -> Mor a -> Mor a
twist'of nm x = let f = (arrow nm x x) in Transform "twist" f [x]
twist :: Mor String -> Mor String
twist x = twist'of "\\theta" x
twist'r :: Mor String -> Mor String
twist'r x = twist'of ("*\\theta") x
untwist'of :: (Eq a) => a -> Mor a -> Mor a
untwist'of nm x = let f = (arrow nm x x) in Transform "untwist" f [x]
untwist :: Mor String -> Mor String
untwist x = untwist'of "\\theta^{-1}" x
untwist'r :: Mor String -> Mor String
untwist'r x = untwist'of ("*\\theta^{-1}") x
untwist'rule'Iso'Left :: Rule String
untwist'rule'Iso'Left = (untwist'r obA) \. (twist'r obA) \== obA \* obB
untwist'rule'Iso'Right :: Rule String
untwist'rule'Iso'Right = (twist'r obA) \. (untwist'r obA) \== obA
twist'rule'Id :: Rule String
twist'rule'Id = (twist'r tid) \== tid
twist'rule'Natural :: Rule String
twist'rule'Natural = let f = arrow "f" obA obA in
(twist'r obA) \. f \== f \. (twist'r obA)
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'of :: (Eq a) => Mor a -> Mor a
dagger'of f = Func "dagger" [f] Cofunctor
dagger :: (Eq a) => Mor a -> Mor a
dagger = dagger'of
dagger'r :: (Eq a) => Mor a -> Mor a
dagger'r f = dagger'of f
dagger'rule'Id :: Rule String
dagger'rule'Id = (dagger'r obA) \== obA
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'rule'Inv :: Rule String
dagger'rule'Inv = (dagger'r $ dagger'r obA) \== obA