Monocle 0.0.2 → 0.0.3

raw patch · 7 files changed

+392/−144 lines, 7 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• Monocle.cabal +51/−21
• Monocle.hs +0/−102
• Monocle/Core.hs +94/−16
• Monocle/Markup.hs +25/−2
• Monocle/Rules.hs +219/−0
• Monocle/Tex.hs +2/−2
• monocle-test.hs +1/−1

@@ -1,21 +1,51 @@-Name:                Monocle-Cabal-Version:       >= 1.2-Version:             0.0.2-Synopsis:            Symbolic computations in strict monoidal categories with LaTeX output.-Description:         Symbolic computations in strict monoidal categories with LaTeX output.-                     See monocle-test.hs.-                     One of goals of this project is to develop the tool for automatic -                     drawing of diagrams of morphisms and proofs in form suitable for LaTeX (e.g. for XY-pic).-License:             BSD3-License-file:        LICENSE-Author:              Osman Bineev-Maintainer:          Osman Bineev (bineev AT gmail DOT com)-Category:            Math-Build-type:          Simple-Extra-source-files:  monocle-test.hs-Stability:           alpha--Library-    exposed-modules:     Monocle.Utils, Monocle.Core, Monocle.Markup, Monocle.Tex, Monocle-    build-depends:       base >= 3 && < 5, containers, mtl, haskell98-  +name: Monocle+version: 0.0.3+cabal-version: >=1.2+build-type: Simple+license: BSD3+license-file: LICENSE+copyright:+maintainer: Osman Bineev (bineev AT gmail DOT com)+build-depends: base >=3 && <5, containers -any, haskell98 -any,+               mtl -any+stability: alpha+homepage:+package-url:+bug-reports:+synopsis: Symbolic computations in strict monoidal categories with LaTeX output.+description: Symbolic computations in strict monoidal categories with LaTeX output.+             See monocle-test.hs.+             One of goals of this project is to develop the tool for automatic+             drawing of diagrams of morphisms and proofs in form suitable for LaTeX (e.g. for XY-pic).+category: Math+author: Osman Bineev+tested-with:+data-files:+data-dir: ""+extra-source-files: monocle-test.hs+extra-tmp-files:+exposed-modules: Monocle.Core Monocle.Markup Monocle.Rules+                 Monocle.Tex Monocle.Utils+exposed: True+buildable: True+build-tools:+cpp-options:+cc-options:+ld-options:+pkgconfig-depends:+frameworks:+c-sources:+extensions:+extra-libraries:+extra-lib-dirs:+includes:+install-includes:+include-dirs:+hs-source-dirs: .+other-modules:+ghc-prof-options:+ghc-shared-options:+ghc-options:+hugs-options:+nhc98-options:+jhc-options:

@@ -1,102 +0,0 @@-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-

@@ -1,31 +1,76 @@-module Monocle.Core where+module Monocle.Core (+    -- * Morphism+    Morphism (..),+    FuncT (..),+    Mor (..),+    -- * Basic functions on morphisms+    nrm,+    atomary,+    arrow,+    element,+    coelement,+    object,+    objectId,+    tid,+    -- * Tensor product functoriality+    vert,+    horz,+    -- * Utilities+    collect,+    -- * Rules+    Rule (..),+    (\==),+    apply+    )where  import Monocle.Utils import Control.Monad.State import qualified Data.Map as Map +-- | Class of morphisms. class (Eq a) => Morphism a where+    -- | Returns domain of the given morphism.     dom :: a -> a+    -- | Returns codomain of the given morphism.     cod :: a -> a+    -- | Checks whether morphism is id.     isId :: a -> Bool+    -- | Composition of two morphisms (should be associative).     (\.) :: a -> a -> a+    -- | Tensor product of two morphisms.     (\*) :: a -> a -> a  infixl 7  \* infixl 6  \.  data ArrowData a = ArrowData { dom' :: Mor a, cod' :: Mor a, isId' :: Bool } deriving (Eq, Ord)-data FuncT = Function | Functor | Cofunctor deriving (Eq, Ord) -data Mor a =-    Arrow a (ArrowData a) |-    Id a |-    Tensor [Mor a] |-    Composition [Mor a] |-    Func String [Mor a] FuncT |-    Transform String (Mor a) [Mor a]+-- | Types of the functional modifier.+data FuncT+    -- | Function on objects+    = Function+    -- | Covariant functor+    | Functor+    -- | Contravariant functor+    | Cofunctor     deriving (Eq, Ord) +-- | Morphism data type+data Mor a+    -- | Atomary morphism+    = Arrow a (ArrowData a)+    -- | Identity morphism+    | Id a+    -- | Tensor product of morphisms+    | Tensor [Mor a]+    -- | Composition of morphisms+    | Composition [Mor a]+    -- | Functionional modifier+    | Func String [Mor a] FuncT+    -- | Naturally transformational modifier+    | Transform String (Mor a) [Mor a]+    deriving (Eq, Ord)+ instance (Eq a) => Morphism (Mor a) where     dom x = case x of         Arrow _ dt -> dom' dt@@ -82,8 +127,10 @@             Tensor y -> Tensor ([f]++y)             _ -> Tensor [f, g] --- Basic functions on morphisms:+-- Basic functions on morphisms +-- | Normalizes the term representing morphism, e.g. turns @((a \* b) \* c)@ to @(a \* b \* c)@+nrm :: (Eq t) => Mor t -> Mor t nrm f = case f of     Arrow ff (ArrowData d c ii) -> Arrow ff (ArrowData (nrm d) (nrm c) ii)     Tensor [x] -> x@@ -102,7 +149,9 @@             y:ys -> (uncomp ys) \. y             _ -> Composition x -terminal f = case f of+-- | Checks whether morphism is an atomary formula.+atomary :: (Eq t) => Mor t -> Bool+atomary f = case f of     Arrow _ _ -> True     Id _ -> True     Transform _ _ _ -> True@@ -121,11 +170,28 @@ getData s@(Id _) = ArrowData s s True getData s@_ = ArrowData (dom s) (cod s) (isId s) +-- | Creates 'Arrow' by morphism information (e.g. name), domain and codomain.+arrow :: a -> Mor a -> Mor a -> Mor a arrow nm adom acod = Arrow nm (ArrowData adom acod False)++-- | Creates generalized element, i.e. an arrow from the tensorial Id to the given object.+element :: a -> Mor a -> Mor a element nm acod = arrow nm (Tensor []) acod++-- | Creates generalized coelement, i.e. an arrow from the the given object to the tensorial Id.+coelement :: a -> Mor a -> Mor a coelement nm adom = arrow nm adom (Tensor [])++-- | Creates object (actually it's id). Same as 'objectId'.+object :: a -> Mor a object nm = Id nm++-- | Creates object id. Same as 'object'.+objectId :: a -> Mor a objectId nm = Id nm++-- | Tensorial Id, @tid \* f == f@ in strict monoidal category.+tid :: Mor a tid = Tensor []  width :: (Eq a) => Mor a -> Int@@ -145,8 +211,9 @@     Transform _ x _ -> height x     _ -> 1 --- Tensor product functoriality:+-- Tensor product functoriality +-- | Turns recursively @(a \\* b) \\. (c \\* d)@ to @(a \\. c) \\* (b \\. d)@. vert :: (Eq a) => Mor a -> Mor a vert f = case f of     Composition (y1:y2:[]) -> vertPair y1 y2@@ -175,6 +242,7 @@             Func s xs t -> Func s (map vert xs) t             _ -> f +-- | Turns recursively @(a \\. c) \\* (b \\. d)@ to @(a \\* b) \\. (c \\* d)@. horz :: (Eq a) => Mor a -> Mor a horz f = case f of     Tensor (y1:y2:[]) -> horzPair y1 y2@@ -204,7 +272,7 @@             Func s xs t -> Func s (map horz xs) t             _ -> f --- Monad.State support:+-- Monad.State support  mapMorM :: (Eq a, Monad m) => m () -> (Mor a -> m (Mor a)) -> Mor a -> m (Mor a) mapMorM prep func f = case f of@@ -269,7 +337,7 @@ instance (Printable a, Eq a) => Show (Mor a) where     show f = str f --- Match, substitute etc.+-- Utilities  merge :: (Eq a, Eq b) => Mor a -> Mor b -> Maybe (Mor (Mor a, b)) merge m1 m2 = case (m1, m2) of@@ -336,6 +404,8 @@                 Id f' -> return arr'                 _ -> error $ "subst': no match in " ++ (show arr') +-- | Collects atomary subterms of the given arrow as keys of the map.+collect :: (Num b, Ord a) => Mor a -> Map.Map (Mor a) b collect f = fst $ calcMor' f (Map.empty, 1) $ \x ->     case x of         Arrow _ _ -> do@@ -348,9 +418,15 @@             return x         _ -> return x --- Rules:+-- Rules -data Rule a = DefEqual (Mor a) (Mor a)+-- | Rule type+data Rule a+    -- | Declares equality of two morphisms+    = DefEqual (Mor a) (Mor a)++-- | @x \\== y@ is the same as @'DefEqual' x y@+(\==) :: Mor a -> Mor a -> Rule a x \== y = DefEqual x y  infix 4  \==@@ -358,6 +434,8 @@ r'left (DefEqual x _) = x r'right (DefEqual _ x) = x +-- | Applies the 'Rule' to the given morphism+apply :: (Eq a) => Rule String -> Mor a -> Mor a apply (DefEqual l r) f =     let (tv, mp) = match f l in         if not tv then let (tv, mp) = match f r in

@@ -1,9 +1,18 @@-module Monocle.Markup where+module Monocle.Markup (+    Lab (..),+    markup,+    unmark,+    modif,+    modif',+    modifLab,+    choose,+    getLabel+    )where  import Monocle.Core import Control.Monad.State -+-- | Labelled arrow data type. data Lab a =     MArrow (Mor a) String |     MId (Mor a) String |@@ -28,6 +37,8 @@     Func nm xs t -> MFunc nm (map makeLab xs) t ""     Transform nm x xs -> MTransform nm (makeLab x) xs "" +-- | Removes labels and returns corresponding 'Mor'.+unmark :: (Eq a) => Lab a -> Mor a unmark lf = nrm $ case lf of     MArrow f _ -> f     MId f _ -> f@@ -51,6 +62,8 @@         func $ MTransform nm x' xs lab     _ -> func lf +-- | Returns the label of the given marked morphism.+getLabel :: Lab a -> String getLabel lf = case lf of     MArrow _ lab -> lab     MId _ lab -> lab@@ -73,18 +86,24 @@ transLabP mor inits prep wlk = evalState ((mapLabM prep wlk) mor) inits calcLabP mor inits prep wlk  = execState ((mapLabM prep wlk) mor) inits +-- | Applies operation to the marked subterm of the given morphism.+modifLab :: String -> Lab a -> (Lab a -> Lab a) -> Lab a modifLab s lf op = transLab lf () $ \x ->     let xlab = getLabel x in         if xlab == s then             return $ op x         else return x +-- | Applies operation to the marked subterm of the given morphism.+modif' :: (Eq a) => String -> Lab a -> (Mor a -> Mor a) -> Lab a modif' s lf op = transLab lf () $ \x ->     let xlab = getLabel x in         if xlab == s then             return $ setLabel xlab $ makeLab $ nrm $ op $ unmark x         else return x +-- | @'unmark' $ 'modif'' s lf op@+modif :: (Eq a) => String -> Lab a -> (Mor a -> Mor a) -> Mor a modif s lf op = unmark $ modif' s lf op  getByLab s f = calcLab f Nothing $ \x ->@@ -100,6 +119,8 @@     put $ (getLabel x, unmark x):ls     return x +-- | Chooses subterm of an associative operation (composition or tensor product).+choose :: String -> Int -> Int -> Lab a -> Lab a choose nlab start end f = case f of     MTensor xs lab -> let ((xs1, xs2), xs3) = (let (x1, x2) = splitAt end xs in (splitAt (start-1) x1, x2)) in             MTensor (xs1 ++ [MTensor xs2 nlab] ++ xs3) lab@@ -108,6 +129,8 @@             MComposition (xs1 ++ [MComposition xs2 nlab] ++ xs3) lab     _ -> error "choose: arrow is not composition or tensor" +-- | Returns the given morphism marked up.+markup :: Mor a -> Lab a markup f = transLab (makeLab f) 1 $ \x ->     case x of         MComposition _ _ -> do

@@ -0,0 +1,219 @@+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'.+untwist'rule'Iso'Left :: Rule String+untwist'rule'Iso'Left = (untwist'r obA) \. (twist'r obA) \== obA \* obB++-- | Isomorphism rule: 'twist' as inverse of 'untwist'.+untwist'rule'Iso'Right :: Rule String+untwist'rule'Iso'Right = (twist'r obA) \. (untwist'r obA) \== obA++-- | Twisting tensorial Id 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' swaps domain and codomain.+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 = (dagger'r $ dagger'r obA) \== obA+

@@ -95,7 +95,7 @@ instance (Printable a, Ord a) => Texified (Mor a) where     tex f = t'math $ t'open $ t'texMor f -    doc f = if terminal f then+    doc f = if atomary f then         if not $ isId f then t'docHead_ t'texMor t'objMor "morphism " f else ""         else t'doc_ t'texMor t'objMor "morphism " f $ collect f @@ -139,7 +139,7 @@ instance (Printable a, Ord a) => Texified (Lab a) where     tex f = t'math $ t'open $ t'texLab f -    doc f = if terminal $ unmark f then+    doc f = if atomary $ unmark f then         if not $ isId f then t'docHead_ t'texLab t'objLab "marked morphism " f else ""         else t'doc_ t'texLab t'objLab "marked morphism " f $ collect $ unmark f 

@@ -3,7 +3,7 @@ import Monocle.Core import Monocle.Tex import Monocle.Markup-import Monocle+import Monocle.Rules  main = do