diff --git a/ChangeLog b/ChangeLog
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,4 @@
+0.9.4: Added tmap and laws
 0.9.3: Not awake
 0.9.2: Fixed some very small errors
 0.9.1: Fixed some typos in the docs
diff --git a/Data/TASequence.hs b/Data/TASequence.hs
--- a/Data/TASequence.hs
+++ b/Data/TASequence.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE GADTs,TypeSynonymInstances,FlexibleInstances #-}
+{-# LANGUAGE GADTs,TypeSynonymInstances,FlexibleInstances,Rank2Types #-}
 
 
 
@@ -45,22 +45,61 @@
 infixr 5 <|
 infixl 5 |>
 infix 5 ><
+{- | A type class for type aligned sequences
+ 
+Minimal complete defention: 'tempty' and 'tsingleton' and ('tviewl' or 'tviewr') and ('><' or '|>' or '<|')
 
--- | minimal complete defention: 'tempty' and 'tsingleton' and ('tviewl' or 'tviewr') and ('><' or '|>' or '<|')
+Instances should satisfy the following laws:
+
+Category laws:
+> tempty >< x == x
+> x >< tempty == x
+> (x >< y) >< z = x >< (y >< z)
+
+Observation laws:
+> tviewl (tsingleton e >< s) == e :< s
+> tviewl tempty == TAEmptyL
+
+The behaviour of '<|','|>', 'tmap' and 'tviewr' is implied by the above laws and their default definitions.
+-}
 class TASequence s where
 
   tempty     :: s c x x
   tsingleton :: c x y -> s c x y
   -- | Append two type aligned sequences
   (><)       :: s c x y -> s c y z  -> s c x z
-  -- | View the type aligned sequence from the left
+  -- | View a type aligned sequence from the left
   tviewl     :: s c x y -> TAViewL s c x y
-  -- | View the type aligned sequence from the right
+{- | View a type aligned sequence from the right
+         
+Default definition:
+> tviewr q = case tviewl q of 
+>   TAEmptyL -> TAEmptyR
+>   h :< t -> case tviewr t of
+>        TAEmptyR -> tempty   :> h
+>        p :> l   -> (h <| p) :> l
+-}
   tviewr     :: s c x y -> TAViewR s c x y
-  -- | Append a single element to the right
+{- | Append a single element to the right
+
+Default definition:
+> l |> r = l >< tsingleton r
+-}
   (|>)       :: s c x y -> c y z -> s c x z
-  -- | Append a single element to the left
+{- | Append a single element to the left
+
+Default definition:
+> l <| r = tsingleton l >< r
+-}
   (<|)       :: c x y -> s c y z -> s c x z
+{- | Apply a function to all elements in a type aligned sequence
+
+Default definition:
+> tmap f q = case tviewl q of
+>    TAEmptyL -> tempty
+>    h :< t -> f h <| tmap f t
+-}
+  tmap       :: (forall x y. c x y -> d x y) -> s c x y -> s d x y
   
   l |> r = l >< tsingleton r
   l <| r = tsingleton l >< r
@@ -80,7 +119,11 @@
         TAEmptyR -> tempty   :> h
         p :> l   -> (h <| p) :> l
 
+  tmap f q = case tviewl q of
+    TAEmptyL -> tempty
+    h :< t -> f h <| tmap f t
 
+
 data TAViewL s c x y where
    TAEmptyL  :: TAViewL s c x x
    (:<)     :: c x y -> s c y z -> TAViewL s c x z
@@ -89,8 +132,6 @@
    TAEmptyR  :: TAViewR s c x x
    (:>)     :: s c x y -> c y z -> TAViewR s c x z
 
-
-
 instance TASequence s => Category (s c) where
   id = tempty
-  (.) = flip (><) -- not (><): type error
+  (.) = flip (><)
diff --git a/Data/TASequence/BinaryTree.hs b/Data/TASequence/BinaryTree.hs
--- a/Data/TASequence/BinaryTree.hs
+++ b/Data/TASequence/BinaryTree.hs
@@ -34,3 +34,6 @@
   tviewl (Node (Leaf c) r)   = c :< r
   tviewl (Node Empty r)      = tviewl r
                         
+  tmap phi Empty = Empty
+  tmap phi (Leaf c) = Leaf (phi c)
+  tmap phi (Node b b') = Node (tmap phi b) (tmap phi b')
diff --git a/Data/TASequence/ConsList.hs b/Data/TASequence/ConsList.hs
--- a/Data/TASequence/ConsList.hs
+++ b/Data/TASequence/ConsList.hs
@@ -27,3 +27,5 @@
   (<|) = Cons
   tviewl CNil = TAEmptyL
   tviewl (Cons h t) = h :< t
+
+  
diff --git a/Data/TASequence/FastQueue.hs b/Data/TASequence/FastQueue.hs
--- a/Data/TASequence/FastQueue.hs
+++ b/Data/TASequence/FastQueue.hs
@@ -48,3 +48,4 @@
  tviewl (RQ CNil SNil CNil) = TAEmptyL
  tviewl (RQ (h `Cons` t) f a) = h :< queue t f a
 
+ tmap phi (RQ a b c) = RQ (tmap phi a) (tmap phi b) (tmap phi c)
diff --git a/Data/TASequence/FingerTree.hs b/Data/TASequence/FingerTree.hs
--- a/Data/TASequence/FingerTree.hs
+++ b/Data/TASequence/FingerTree.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE GADTs #-}
+{-# LANGUAGE Rank2Types,GADTs #-}
 
 
 
@@ -31,7 +31,6 @@
   Single :: r a b -> FingerTree r a b
   Deep   :: !(Digit r a b) -> FingerTree (Node r) b c -> !(Digit r c d) -> FingerTree r a d
 
-
 data Node r a b where
   Node2 :: r a b -> r b c -> Node r a c
   Node3 :: r a b -> r b c -> r c d -> Node r a d
@@ -68,8 +67,12 @@
 
   xs >< ys = app3 xs ZNil ys
 
+  tmap f Empty = Empty
+  tmap f (Single a) = Single (f a)
+  tmap f (Deep l m r) = Deep (mapd f l) (tmap (mapn f) m) (mapd f r)
 
 
+
 toTree :: Digit r a b -> FingerTree r a b
 toTree (One a)         = Single a
 toTree (Two a b)       = Deep (One a) Empty (One b)
@@ -185,5 +188,15 @@
 nodes (a ::: b ::: c ::: ZNil) = Node3 a b c ::: ZNil
 nodes (a ::: b ::: c ::: d ::: ZNil) = Node2 a b ::: Node2 c d ::: ZNil
 nodes (a ::: b ::: c ::: xs) = Node3 a b c ::: nodes xs
+
+mapn :: (forall x y. c x y -> d x y) -> Node c x y -> Node d x y
+mapn phi (Node2 r s) = Node2 (phi r) (phi s)
+mapn phi (Node3 r s t) = Node3 (phi r) (phi s) (phi t)
+  
+mapd :: (forall x y. c x y -> d x y) -> Digit c x y -> Digit d x y
+mapd phi (One r) = One (phi r) 
+mapd phi (Two r s) = Two (phi r) (phi s)
+mapd phi (Three r s t) = Three (phi r) (phi s) (phi t)
+mapd phi (Four r s t u) = Four (phi r) (phi s) (phi t) (phi u)
 
 
diff --git a/Data/TASequence/Queue.hs b/Data/TASequence/Queue.hs
--- a/Data/TASequence/Queue.hs
+++ b/Data/TASequence/Queue.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE GADTs, DataKinds, TypeOperators #-}
+{-# LANGUAGE Rank2Types,GADTs, DataKinds, TypeOperators #-}
 
 
 
@@ -55,5 +55,13 @@
                l :< m -> QN (B2 l) m r
            buf2queue (B1 a)        = Q1 a
            buf2queue(B2 (a :* b))  = QN (B1 a) Q0 (B1 b)
+  tmap f Q0 = Q0
+  tmap f (Q1 x) = Q1 (f x)
+  tmap f (QN l m r) = QN (tmapb f l) (tmap (tmapp f) m) (tmapb f r)
+
+tmapp :: (forall x y. c x y -> d x y) -> P c x y -> P d x y
+tmapp phi (a :* b) = phi a :* phi b
   
-             
+tmapb :: (forall x y. c x y -> d x y) -> B c x y -> B d x y
+tmapb phi (B1 c) = B1 (phi c)
+tmapb phi (B2 p) = B2 (tmapp phi p)
diff --git a/Data/TASequence/SnocList.hs b/Data/TASequence/SnocList.hs
--- a/Data/TASequence/SnocList.hs
+++ b/Data/TASequence/SnocList.hs
@@ -28,3 +28,5 @@
   (|>) = Snoc
   tviewr SNil = TAEmptyR
   tviewr (Snoc p l) = p :> l
+  tmap phi SNil = SNil
+  tmap phi (Snoc s c) = Snoc (tmap phi s) (phi c)
diff --git a/Data/TASequence/ToCatQueue.hs b/Data/TASequence/ToCatQueue.hs
--- a/Data/TASequence/ToCatQueue.hs
+++ b/Data/TASequence/ToCatQueue.hs
@@ -46,3 +46,6 @@
      CN x q :< t  -> CN x (q `snoc` linkAll t)
     snoc q C0  = q
     snoc q r   = q |> r
+
+ tmap phi C0 = C0
+ tmap phi (CN c q) = CN (phi c) (tmap (tmap phi) q)
diff --git a/type-aligned.cabal b/type-aligned.cabal
--- a/type-aligned.cabal
+++ b/type-aligned.cabal
@@ -1,5 +1,5 @@
 Name:                type-aligned
-Version:             0.9.3
+Version:             0.9.4
 Synopsis:	         Various type-aligned sequence data structures.
 Description:         Various data structures for type aligned sequences: heterogeneous sequences where the types enforce the element order.
 License:             BSD3
@@ -14,9 +14,9 @@
 Tested-With:         GHC==7.6.3
 Library
   Build-Depends: base >= 2 && <= 6
-  Exposed-modules: Data.TASequence, Data.TASequence.BinaryTree, Data.TASequence.ConsList, Data.TASequence.FastCatQueue,  Data.TASequence.FastQueue, Data.TASequence.FingerTree, Data.TASequence.Queue, Data.TASequence.SnocList, Data.TASequence.ToCatQueue
+  Exposed-modules: Data.TASequence.BinaryTree, Data.TASequence, Data.TASequence.ConsList, Data.TASequence.FastCatQueue,  Data.TASequence.FastQueue, Data.TASequence.FingerTree, Data.TASequence.Queue, Data.TASequence.SnocList, Data.TASequence.ToCatQueue
 
-  Extensions:	 GADTs, TypeSynonymInstances,FlexibleInstances, ViewPatterns, TypeOperators
+  Extensions:	 GADTs, ViewPatterns, TypeOperators, Rank2Types
 
 source-repository head
     type:     git