--- a/agda/delta.agda	Mon Jan 26 14:08:46 2015 +0900
+++ b/agda/delta.agda	Mon Jan 26 23:00:05 2015 +0900
@@ -1,6 +1,7 @@
 open import list
 open import basic
 open import nat
+open import revision
 open import laws
 
 open import Level
@@ -9,59 +10,56 @@
 
 module delta where
 
+data Delta {l : Level} (A : Set l) : (Rev -> (Set l)) where
+  mono    : A -> Delta A init
+  delta   : {v : Rev} -> A -> Delta A v -> Delta A (commit v)
 
-data Delta {l : Level} (A : Set l) : (Set l) where
-  mono    : A -> Delta A
-  delta   : A -> Delta A -> Delta A
-
-deltaAppend : {l : Level} {A : Set l} -> Delta A -> Delta A -> Delta A
+deltaAppend : {l : Level} {A : Set l} {n m : Rev} -> Delta A n -> Delta A m -> Delta A (merge n m)
 deltaAppend (mono x) d     = delta x d
 deltaAppend (delta x d) ds = delta x (deltaAppend d ds)
 
-headDelta : {l : Level} {A : Set l} -> Delta A -> A
+headDelta : {l : Level} {A : Set l} {n : Rev} -> Delta A n -> A
 headDelta (mono x)    = x
 headDelta (delta x _) = x
 
-tailDelta : {l : Level} {A : Set l} -> Delta A -> Delta A
-tailDelta (mono x)    = mono x
+tailDelta : {l : Level} {A : Set l} {n : Rev} -> Delta A (commit n) -> Delta A n
 tailDelta (delta _ d) = d
 
-n-tail : {l : Level} {A : Set l} -> Nat -> ((Delta A) -> (Delta A))
-n-tail O = id
-n-tail (S n) =  tailDelta ∙ (n-tail n)
 
 
 -- Functor
-delta-fmap : {l : Level} {A B : Set l} -> (A -> B) -> (Delta A) -> (Delta B)
+delta-fmap : {l : Level} {A B : Set l} {n : Rev} -> (A -> B) -> (Delta A n) -> (Delta B n)
 delta-fmap f (mono x)    = mono  (f x)
 delta-fmap f (delta x d) = delta (f x) (delta-fmap f d)
 
 
 
 -- Monad (Category)
-delta-eta : {l : Level} {A : Set l} -> A -> Delta A
-delta-eta x = mono x
+delta-eta : {l : Level} {A : Set l} {v : Rev} -> A -> Delta A v
+delta-eta {v = init} x     = mono x
+delta-eta {v = commit v} x = delta x (delta-eta {v = v} x)
 
-delta-bind : {l : Level} {A B : Set l} -> (Delta A) -> (A -> Delta B) -> Delta B
-delta-bind (mono x)    f = f x
-delta-bind (delta x d) f = delta (headDelta (f x)) (delta-bind d (tailDelta ∙ f))
+delta-bind : {l : Level} {A B : Set l} {n : Rev} -> (Delta A n) -> (A -> Delta B n) -> Delta B n
+delta-bind (mono x) f    = f x
+delta-bind (delta x d) f = delta (headDelta (f x)) (tailDelta (f x))
 
-delta-mu : {l : Level} {A : Set l} -> Delta (Delta A) -> Delta A
+delta-mu : {l : Level} {A : Set l} {n : Rev} -> (Delta (Delta A n) n) -> Delta A n
 delta-mu d = delta-bind d id
 
 
 
+{-
 -- Monad (Haskell)
-delta-return : {l : Level} {A : Set l} -> A -> Delta A
+delta-return : {l : Level} {A : Set l} -> A -> Delta A (S O)
 delta-return = delta-eta
 
-_>>=_ : {l : Level} {A B : Set l} ->
-        (x : Delta A) -> (f : A -> (Delta B)) -> (Delta B)
-(mono x)    >>= f = f x
-(delta x d) >>= f = delta (headDelta (f x)) (d >>= (tailDelta ∙ f))
+_>>=_ : {l : Level} {A B : Set l} {n : Nat} ->
+        (x : Delta A n) -> (f : A -> (Delta B n)) -> (Delta B n)
+d >>= f = delta-bind d f
 
+-}
 
-
+{-
 -- proofs
 
 -- sub-proofs
@@ -122,3 +120,4 @@
   delta-fmap f (n-tail n d)                               ≡⟨ refl ⟩
   delta-fmap f (((n-tail n) ∙ tailDelta) (delta x d))     ≡⟨ cong (\t -> delta-fmap f (t (delta x d))) (n-tail-plus n) ⟩
   delta-fmap f (n-tail (S n) (delta x d))                 ∎
+-}