diff --git a/Monocle.cabal b/Monocle.cabal
--- a/Monocle.cabal
+++ b/Monocle.cabal
@@ -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:
diff --git a/Monocle.hs b/Monocle.hs
deleted file mode 100644
--- a/Monocle.hs
+++ /dev/null
@@ -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
-
diff --git a/Monocle/Core.hs b/Monocle/Core.hs
--- a/Monocle/Core.hs
+++ b/Monocle/Core.hs
@@ -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
diff --git a/Monocle/Markup.hs b/Monocle/Markup.hs
--- a/Monocle/Markup.hs
+++ b/Monocle/Markup.hs
@@ -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
diff --git a/Monocle/Rules.hs b/Monocle/Rules.hs
new file mode 100644
--- /dev/null
+++ b/Monocle/Rules.hs
@@ -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
+
diff --git a/Monocle/Tex.hs b/Monocle/Tex.hs
--- a/Monocle/Tex.hs
+++ b/Monocle/Tex.hs
@@ -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
 
diff --git a/monocle-test.hs b/monocle-test.hs
--- a/monocle-test.hs
+++ b/monocle-test.hs
@@ -3,7 +3,7 @@
 import Monocle.Core
 import Monocle.Tex
 import Monocle.Markup
-import Monocle
+import Monocle.Rules
 
 main = do