diff --git a/ot.cabal b/ot.cabal
--- a/ot.cabal
+++ b/ot.cabal
@@ -1,5 +1,5 @@
 Name:                ot
-Version:             0.2.0.0
+Version:             0.2.1.0
 Synopsis:            Real-time collaborative editing with Operational Transformation
 -- A longer description of the package.
 -- Description:         
@@ -22,9 +22,9 @@
   Exposed-modules:     Control.OperationalTransformation, Control.OperationalTransformation.List, Control.OperationalTransformation.Text, Control.OperationalTransformation.Selection, Control.OperationalTransformation.Properties, Control.OperationalTransformation.Client, Control.OperationalTransformation.Server
   Build-depends:       base >= 4 && < 5,
                        text >= 1.0 && < 1.3,
-                       aeson >= 0.7 && < 0.9,
+                       aeson >= 0.7 && < 0.11,
                        attoparsec >= 0.10.1.1 && < 1,
-                       QuickCheck >= 2.7 && < 2.8,
+                       QuickCheck >= 2.7 && < 2.9,
                        binary >= 0.5.1.1 && < 0.8,
                        either >= 4.1.2 && < 5,
                        mtl >= 2.1.3.1 && < 3,
diff --git a/src/Control/OperationalTransformation/Properties.hs b/src/Control/OperationalTransformation/Properties.hs
--- a/src/Control/OperationalTransformation/Properties.hs
+++ b/src/Control/OperationalTransformation/Properties.hs
@@ -1,9 +1,22 @@
+{-# LANGUAGE DataKinds, ConstraintKinds, KindSignatures, GADTs #-}
+{-# LANGUAGE FlexibleInstances, FlexibleContexts, MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableInstances, ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+
 module Control.OperationalTransformation.Properties
-  ( prop_compose_apply
-  , prop_transform_apply
-  , prop_transform_compose
+  ( ArbitraryFor (..)
+  -- , TestableOTSystem
+  -- , ArbitraryOTSystem
+  , Nat (..), One, Two, Three
+  , DocHistory (..)
+  , ConcurrentDocHistories (..)
+  , prop_compose_assoc
+  , prop_apply_functorial
+  , prop_transform_apply_comm
+  , prop_transform_comm
   , prop_transform_compose_compat_l
   , prop_transform_compose_compat_r
+  , prop_transform_functorial
   ) where
 
 import Control.OperationalTransformation
@@ -11,55 +24,140 @@
 import Test.QuickCheck.Property
 import Control.Applicative ((<$>), (<*>))
 
+{-
+type ArbitraryOTSystem doc op =
+  ( OTSystem doc op, OTComposableOperation op
+  , Arbitrary doc, ArbitraryFor doc op --Arbitrary (GenOp doc op)
+  , Show doc, Eq doc, Show op, Eq op
+  )
+-}
+
+type TestableOTSystem doc op =
+  ( OTSystem doc op, OTComposableOperation op
+  --, Arbitrary doc, ArbitraryFor doc op --Arbitrary (GenOp doc op)
+  , Show doc, Eq doc, Show op, Eq op
+  )
+
+class ArbitraryFor a b where
+  arbitraryFor :: a -> Gen b
+
+genOp :: (OTSystem doc op, ArbitraryFor doc op) => doc -> Gen (op, doc)
+genOp doc = do
+  op <- arbitraryFor doc
+  case apply op doc of
+    Left err -> fail err
+    Right doc' -> return (op, doc')
+
+
+data Nat = Z | S !Nat deriving (Eq, Show)
+
+type One = S Z
+type Two = S One
+type Three = S Two
+
+data DocHistory doc op :: Nat -> * where
+  -- | Last state
+  LS :: doc -> DocHistory doc op Z
+  -- | Snapshot
+  SS :: doc -> op -> DocHistory doc op n -> DocHistory doc op (S n)
+
+deriving instance (Show doc, Show op) => Show (DocHistory doc op n)
+deriving instance (Eq doc, Eq op) => Eq (DocHistory doc op n)
+
+data ConcurrentDocHistories doc op n k =
+  CDH (DocHistory doc op n) (DocHistory doc op k)
+
+deriving instance (Show doc, Show op) => Show (ConcurrentDocHistories doc op n k)
+deriving instance (Eq doc, Eq op) => Eq (ConcurrentDocHistories doc op n k)
+
+{-
+getCurrentState :: DocHistory doc op n -> doc
+getCurrentState (LS doc) = doc
+getCurrentState (SS _ _ dh) = getCurrentState dh
+
+snocDocHistory :: DocHistory doc op n -> op -> doc -> DocHistory doc op (S n)
+snocDocHistory (LS doc) op doc' = SS doc op (LS doc')
+snocDocHistory (SS doc op dh) op' doc' = SS doc op (snocDocHistory dh op' doc')
+-}
+
+instance ArbitraryFor doc (DocHistory doc op Z) where
+  arbitraryFor = return . LS
+
+instance (OTSystem doc op, ArbitraryFor doc op, ArbitraryFor doc (DocHistory doc op n)) => ArbitraryFor doc (DocHistory doc op (S n)) where
+  arbitraryFor doc = do
+    (op, doc') <- genOp doc
+    SS doc op <$> arbitraryFor doc'
+
+instance (Arbitrary doc, ArbitraryFor doc (DocHistory doc op n)) => Arbitrary (DocHistory doc op n) where
+  arbitrary = (arbitrary :: Gen doc) >>= arbitraryFor
+
+instance (ArbitraryFor doc (DocHistory doc op n), ArbitraryFor doc (DocHistory doc op k)) => ArbitraryFor doc (ConcurrentDocHistories doc op n k) where
+  arbitraryFor doc = CDH <$> arbitraryFor doc <*> arbitraryFor doc
+
+instance (Arbitrary doc, ArbitraryFor doc (ConcurrentDocHistories doc op n k)) => Arbitrary (ConcurrentDocHistories doc op n k) where
+  arbitrary = (arbitrary :: Gen doc) >>= arbitraryFor
+
 (==?) :: (Eq a, Show a) => a -> a -> Result
 a ==? b | a == b    = succeeded
         | otherwise = failed { reason = "expected " ++ show a ++ " to be " ++ show b }
 
-eitherProperty :: (Either String a) -> (a -> Property) -> Property
+eitherResult :: Either String a -> (a -> Result) -> Result
+eitherResult (Left err) _ = failed { reason = err }
+eitherResult (Right a) f  = f a
+
+eitherProperty :: Either String a -> (a -> Property) -> Property
 eitherProperty (Left err) _ = property $ failed { reason = err }
 eitherProperty (Right res) prop = prop res
 
+prop_compose_assoc
+  :: TestableOTSystem doc op
+  => DocHistory doc op Three
+  -> Result
+prop_compose_assoc (SS _doc a (SS _ b (SS _ c _))) =
+  eitherResult (compose a b) $ \ab ->
+  eitherResult (compose ab c) $ \abc1 ->
+  eitherResult (compose b c) $ \bc ->
+  eitherResult (compose a bc) $ \abc2 ->
+  abc1 ==? abc2
+
 -- | @(b ∘ a)(d) = a(b(d))@ where /a/ and /b/ are two consecutive operations
 -- and /d/ is the initial document.
-prop_compose_apply :: (OTSystem doc op, OTComposableOperation op, Arbitrary doc, Show doc, Eq doc)
-                   => (doc -> Gen op) -> Property
-prop_compose_apply genOperation = property $ do
-  doc <- arbitrary
-  a <- genOperation doc
-  return $ eitherProperty (apply a doc) $ \doc' -> property $ do
-    b <- genOperation doc'
-    return $ eitherProperty ((,) <$> apply b doc' <*> compose a b) $ \(doc'', ab) ->
-      property $ Right doc'' ==? apply ab doc
+prop_apply_functorial
+  :: TestableOTSystem doc op
+  => DocHistory doc op Two
+  -> Result
+prop_apply_functorial (SS doc a (SS _ b (LS _))) =
+  eitherResult (apply a doc) $ \doc' ->
+  eitherResult (apply b doc') $ \doc''1 ->
+  eitherResult (compose a b) $ \ab ->
+  eitherResult (apply ab doc) $ \doc''2 ->
+  doc''1 ==? doc''2
 
 -- | @b'(a(d)) = a'(b(d))@ where /a/ and /b/ are random operations, /d/ is the
 -- initial document and @(a', b') = transform(a, b)@.
-prop_transform_apply :: (OTSystem doc op, Arbitrary doc, Show doc, Eq doc)
-                     => (doc -> Gen op)
-                     -> Property
-prop_transform_apply genOperation = property $ do
-  doc <- arbitrary
-  a <- genOperation doc
-  b <- genOperation doc
-  let res1 = (,,) <$> apply a doc <*> apply b doc <*> transform a b
-  return $ eitherProperty res1 $ \(doca, docb, (a', b')) ->
-    let res2 = (,) <$> apply b' doca <*> apply a' docb
-    in eitherProperty res2 $ \(docab', docba') ->
-      property $ docab' ==? docba'
+prop_transform_apply_comm
+  :: TestableOTSystem doc op
+  => ConcurrentDocHistories doc op One One
+  -> Result
+prop_transform_apply_comm (CDH (SS _ a (LS docA)) (SS _ b (LS docB))) =
+  eitherResult (transform a b) $ \(a', b') ->
+  eitherResult (apply a' docB) $ \doc''1 ->
+  eitherResult (apply b' docA) $ \doc''2 ->
+  doc''1 ==? doc''2
 
 -- | @b' ∘ a = a' ∘ b@ where /a/ and /b/ are random operations and
 -- @(a', b') = transform(a, b)@. Note that this is a stronger property than
--- prop_transform_apply, because prop_transform_compose and
--- prop_compose_apply imply prop_transform_apply.
-prop_transform_compose :: (OTSystem doc op, OTComposableOperation op, Arbitrary doc, Show op, Eq op)
-                      => (doc -> Gen op)
-                      -> Property
-prop_transform_compose genOperation = property $ do
-  doc <- arbitrary
-  a <- genOperation doc
-  b <- genOperation doc
-  return $ eitherProperty (transform a b) $ \(a', b') ->
-    eitherProperty ((,) <$> compose a b' <*> compose b a') $ \(ab', ba') ->
-      property $ ab' ==? ba'
+-- 'prop_transform_apply_comm', because 'prop_transform_comm' and
+-- 'prop_apply_functorial' imply 'prop_transform_apply_comm'.
+prop_transform_comm
+  :: TestableOTSystem doc op
+  => ConcurrentDocHistories doc op One One
+  -> Result
+prop_transform_comm (CDH (SS _ a _) (SS _ b _)) =
+  eitherResult (transform a b) $ \(a', b') ->
+  eitherResult (compose a b') $ \ab' ->
+  eitherResult (compose b a') $ \ba' ->
+  ab' ==? ba'
 
 -- | Transformation is compatible with composition on the left. That is, if we
 -- have two consecutive operations /a/ and /b/ and a concurrent operation /c/,
@@ -67,14 +165,15 @@
 -- then against /b/ or transform /c/ against the composition of /a/ and /b/.
 -- In other terms, @c'_1 = c'_2@ where @(_, c'_1) = transform(b ∘ a, c)@,
 -- @(_, c') = transform(a, c)@ and @(_, c'_2) = transform(b, c')@.
-prop_transform_compose_compat_l :: (OTSystem doc op, OTComposableOperation op, Arbitrary doc, Show op, Eq op)
-                                => (doc -> Gen op)
-                                -> Property
+prop_transform_compose_compat_l
+  :: (OTSystem doc op, OTComposableOperation op, Arbitrary doc, Show op, Eq op)
+  => (doc -> Gen op)
+  -> Property
 prop_transform_compose_compat_l genOperation = property $ do
   doc <- arbitrary
   a <- genOperation doc
   c <- genOperation doc
-  return $ eitherProperty (apply a doc) $ \(doc') -> property $ do
+  return $ eitherProperty (apply a doc) $ \doc' -> property $ do
     b <- genOperation doc'
     let res = (,) <$> (snd <$> (compose a b >>= flip transform c))
                   <*> (snd <$> (transform a c >>= transform b . snd))
@@ -82,15 +181,29 @@
       property $ c'_1 ==? c'_2
 
 -- | Transformation is compatible with composition on the /right/.
-prop_transform_compose_compat_r :: (OTSystem doc op, OTComposableOperation op, Arbitrary doc, Show op, Eq op)
-                                => (doc -> Gen op)
-                                -> Property
+prop_transform_compose_compat_r
+  :: (OTSystem doc op, OTComposableOperation op, Arbitrary doc, Show op, Eq op)
+  => (doc -> Gen op)
+  -> Property
 prop_transform_compose_compat_r genOperation = property $ do
   doc <- arbitrary
   a <- genOperation doc
   c <- genOperation doc
-  return $ eitherProperty (apply a doc) $ \(doc') -> property $ do
+  return $ eitherProperty (apply a doc) $ \doc' -> property $ do
     b <- genOperation doc'
     let res = (,) <$> (fst <$> (compose a b >>= transform c))
                   <*> (fst <$> (transform c a >>= flip transform b . fst))
     return $ eitherProperty res $ \(c'_1, c'_2) -> property $ c'_1 ==? c'_2
+
+-- second functor axiom (F(f . g) = Ff . Fg) for F = transform c
+prop_transform_functorial
+  :: TestableOTSystem doc op
+  => ConcurrentDocHistories doc op One Two
+  -> Result
+prop_transform_functorial (CDH (SS _ c _) (SS _ a (SS _ b _))) =
+  eitherResult (compose a b) $ \ab ->
+  eitherResult (transform c ab) $ \(_c''1, abPrimed1) ->
+  eitherResult (transform c a) $ \(c', a') ->
+  eitherResult (transform c' b) $ \(_c''2, b') ->
+  eitherResult (compose a' b') $ \abPrimed2 ->
+  abPrimed1 ==? abPrimed2
diff --git a/src/Control/OperationalTransformation/Text.hs b/src/Control/OperationalTransformation/Text.hs
--- a/src/Control/OperationalTransformation/Text.hs
+++ b/src/Control/OperationalTransformation/Text.hs
@@ -176,9 +176,10 @@
       loop _ _ _ = Left "operation can't be applied to the document: text is longer than the operation"
 
 -- | Computes the inverse of an operation. Useful for implementing undo.
-invertOperation :: TextOperation               -- ^ An operation
-                -> T.Text                      -- ^ Document to apply the operation to
-                -> Either String TextOperation
+invertOperation
+  :: TextOperation               -- ^ An operation
+  -> T.Text                      -- ^ Document to apply the operation to
+  -> Either String TextOperation
 invertOperation (TextOperation actions) doc = loop actions doc []
   where
     loop (op:ops) text inv = case op of