# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1416989493 -32400
# Node ID 6d0193011f899cea3f8a2f4b900857885359a286
# Parent  15eec529dfc4d1eee9a03a6ef17671c377761bb7
Trying prove monad-law-1 by another pattern

diff -r 15eec529dfc4 -r 6d0193011f89 agda/delta.agda
--- a/agda/delta.agda	Wed Nov 26 16:17:53 2014 +0900
+++ b/agda/delta.agda	Wed Nov 26 17:11:33 2014 +0900
@@ -41,7 +41,7 @@
 bind (delta x d) f = deltaAppend (headDelta (f x)) (bind d (tailDelta ∙ f))
 
 mu : {l : Level} {A : Set l} -> Delta (Delta A) -> Delta A
-mu d = bind d id 
+mu d = bind d id
 
 
 returnS : {l : Level} {A : Set l} -> A -> Delta A
@@ -66,24 +66,24 @@
 
 -- sub proofs
 
-head-delta-natural-transformation : {l ll : Level} {A : Set l} {B : Set ll} -> 
+head-delta-natural-transformation : {l ll : Level} {A : Set l} {B : Set ll} ->
                                   (f : A -> B) (d : Delta A) -> (headDelta (fmap f d)) ≡ fmap f (headDelta d)
 head-delta-natural-transformation f (mono x)    = refl
 head-delta-natural-transformation f (delta x d) = refl
 
-tail-delta-natural-transfomation  : {l ll : Level} {A : Set l} {B : Set ll} -> 
+tail-delta-natural-transfomation  : {l ll : Level} {A : Set l} {B : Set ll} ->
                                   (f : A -> B) (d : Delta A) -> (tailDelta (fmap f d)) ≡ fmap f (tailDelta d)
 tail-delta-natural-transfomation f (mono x) = refl
 tail-delta-natural-transfomation f (delta x d) = refl
 
-delta-append-natural-transfomation : {l ll : Level} {A : Set l} {B : Set ll} -> 
-                                  (f : A -> B) (d : Delta A) (dd : Delta A) -> 
+delta-append-natural-transfomation : {l ll : Level} {A : Set l} {B : Set ll} ->
+                                  (f : A -> B) (d : Delta A) (dd : Delta A) ->
                                   deltaAppend (fmap f d) (fmap f dd) ≡ fmap f (deltaAppend d dd)
 delta-append-natural-transfomation f (mono x) dd    = refl
 delta-append-natural-transfomation f (delta x d) dd = begin
-  deltaAppend (fmap f (delta x d)) (fmap f dd) 
+  deltaAppend (fmap f (delta x d)) (fmap f dd)
   ≡⟨ refl ⟩
-  deltaAppend (delta (f x) (fmap f d)) (fmap f dd) 
+  deltaAppend (delta (f x) (fmap f d)) (fmap f dd)
   ≡⟨ refl ⟩
   delta (f x) (deltaAppend (fmap f d) (fmap f dd))
   ≡⟨ cong (\d -> delta (f x) d) (delta-append-natural-transfomation f d dd) ⟩
@@ -91,36 +91,6 @@
   ≡⟨ refl ⟩
   fmap f (deltaAppend (delta x d) dd)
   ∎
-{-
-
-mu-head-delta : {l : Level} {A : Set l} -> (d : Delta (Delta A)) -> mu (headDelta d) ≡ headDelta (mu d)
-mu-head-delta (mono (mono x))    = refl
-mu-head-delta (mono (delta x (mono xx))) = begin
- mu (headDelta (mono (delta x (mono xx))))
- ≡⟨ refl ⟩
- bind (headDelta (mono (delta x (mono xx)))) id
- ≡⟨ refl ⟩
- bind (delta x (mono xx)) return
- ≡⟨ refl ⟩
- deltaAppend (headDelta (return x)) (bind (mono xx) (tailDelta ∙ return))
- ≡⟨ refl ⟩
- deltaAppend (headDelta (return x)) ((tailDelta ∙ return) xx)
- ≡⟨ refl ⟩
- deltaAppend (headDelta (mono x)) (tailDelta (mono xx))
- ≡⟨ refl ⟩
- deltaAppend (mono x) (mono xx)
- ≡⟨ refl ⟩
- delta x (mono xx)
- ≡⟨ {!!} ⟩
- headDelta (delta x (mono xx))
- ≡⟨ refl ⟩
- headDelta (bind (mono (delta x (mono xx))) id)
- ≡⟨ refl ⟩
- headDelta (mu (mono (delta x (mono xx))))
-  ∎
-mu-head-delta (mono (delta x (delta x₁ d))) = {!!}
-mu-head-delta (delta d dd) = {!!}
--}
 -- Functor-laws
 
 -- Functor-law-1 : T(id) = id'
@@ -137,293 +107,102 @@
 
 -- Monad-laws (Category)
 
-monad-law-1-5 : {l : Level} {A : Set l} -> (ds : Delta (Delta A)) ->
-  (tailDelta ∙ tailDelta) (bind ds tailDelta)
-  ≡
-  bind ((tailDelta ∙ tailDelta) ds) ((tailDelta ∙ tailDelta) ∙ tailDelta)
-monad-law-1-5 (mono ds) = refl
-monad-law-1-5 (delta (mono x) ds) = {!!}
-monad-law-1-5 (delta (delta x d) ds) = {!!}
-
-monad-law-1-4 : {l : Level} {A : Set l} -> (x : A) -> (ds : Delta (Delta (Delta A))) ->
-  delta x (bind (fmap mu ds) (tailDelta ∙ (tailDelta ∙ tailDelta)))
-  ≡
-  bind (delta (mono x) (bind ds ((tailDelta ∙ tailDelta ) ∙ tailDelta))) (tailDelta ∙ tailDelta)
-monad-law-1-4 x (mono (mono ds)) = refl
-monad-law-1-4 x (mono (delta (mono xx) ds)) = begin
-  delta x (bind (fmap mu (mono (delta (mono xx) ds))) (tailDelta ∙ (tailDelta ∙ tailDelta)))
-  ≡⟨ refl ⟩
-  delta x (bind (mono (mu (delta (mono xx) ds))) (tailDelta ∙ (tailDelta ∙ tailDelta)))
-  ≡⟨ refl ⟩
-  delta x (bind (mono (bind (delta (mono xx) ds) id)) (tailDelta ∙ (tailDelta ∙ tailDelta)))
-  ≡⟨ refl ⟩
-  delta x (bind (mono (deltaAppend (headDelta (mono xx)) (bind  ds tailDelta))) (tailDelta ∙ (tailDelta ∙ tailDelta)))
-  ≡⟨ refl ⟩
-  delta x (bind (mono (deltaAppend (mono xx) (bind  ds tailDelta))) (tailDelta ∙ (tailDelta ∙ tailDelta)))
-  ≡⟨ refl ⟩
-  delta x (bind (mono (delta xx (bind  ds tailDelta))) (tailDelta ∙ (tailDelta ∙ tailDelta)))
-  ≡⟨ refl ⟩
-  delta x ((tailDelta ∙ (tailDelta ∙ tailDelta)) (delta xx (bind  ds tailDelta)))
-  ≡⟨ refl ⟩
-  delta x ((tailDelta ∙ tailDelta) (bind ds tailDelta))
-  ≡⟨ cong (\d -> delta x d) (monad-law-1-5 ds) ⟩
-  delta x (bind ((tailDelta ∙ tailDelta) ds) ((tailDelta ∙ tailDelta) ∙ tailDelta))
-  ≡⟨ refl ⟩
-  deltaAppend (mono x) (bind ((tailDelta ∙ tailDelta) ds) ((tailDelta ∙ tailDelta) ∙ tailDelta))
-  ≡⟨ refl ⟩
-  deltaAppend (headDelta ((tailDelta ∙ tailDelta) (mono x))) (bind ((tailDelta ∙ tailDelta) ds) ((tailDelta ∙ tailDelta) ∙ tailDelta))
-  ≡⟨ refl ⟩
-  bind (delta (mono x) ((tailDelta ∙ tailDelta) ds)) (tailDelta ∙ tailDelta)
-  ≡⟨ refl ⟩ 
-  bind (delta (mono x) (bind (mono (delta (mono xx) ds)) ((tailDelta ∙ tailDelta) ∙ tailDelta))) (tailDelta ∙ tailDelta)
-  ∎
-monad-law-1-4 x (mono (delta (delta x₁ ds) ds₁)) = {!!}
-monad-law-1-4 x (delta ds ds₁) = {!!}
-
-monad-law-1-3 : {l : Level} {A : Set l} -> (ds : Delta (Delta A)) ->
-  tailDelta (bind ds tailDelta) ≡ bind (tailDelta ds) (tailDelta ∙ tailDelta)
-monad-law-1-3 (mono ds)              = refl
-monad-law-1-3 (delta (mono x) ds)    = refl
-monad-law-1-3 (delta (delta x (mono x₁)) ds) = refl
-monad-law-1-3 (delta (delta x (delta x₁ d)) ds) = refl
+monad-law-1-1 : {l : Level} {A : Set l} -> (d : Delta (Delta (Delta A))) ->
+  (fmap mu d) ≡ (bind d tailDelta)
+monad-law-1-1 (mono (mono d))     = refl
+monad-law-1-1 (mono (delta (mono x) ds)) = begin
+ fmap mu (mono (delta (mono x) ds))
+ ≡⟨ refl ⟩
+ mono (mu (delta (mono x) ds))
+ ≡⟨ refl ⟩
+ mono (deltaAppend (headDelta (mono x)) (bind ds tailDelta))
+ ≡⟨ refl ⟩
+ mono (delta x (bind ds tailDelta))
+ ≡⟨ {!!} ⟩ --? 
+ ds
+ ≡⟨ refl ⟩
+ tailDelta (delta (mono x) ds)
+ ≡⟨ refl ⟩
+ bind (mono (delta (mono x) ds)) tailDelta
+ ∎
 
-monad-law-1-sub-sub : {l : Level} {A : Set l} -> (d : Delta (Delta (Delta A))) ->
-  bind (fmap mu d) (tailDelta ∙ tailDelta) ≡ bind (bind d (tailDelta ∙ tailDelta)) (tailDelta ∙ tailDelta)
-monad-law-1-sub-sub (mono (mono d))            = refl
-monad-law-1-sub-sub (mono (delta (mono x) ds)) = begin
-  bind (fmap mu (mono (delta (mono x) ds))) (tailDelta ∙ tailDelta)
-  ≡⟨ refl ⟩
-  bind (mono (mu (delta (mono x) ds))) (tailDelta ∙ tailDelta)
-  ≡⟨ refl ⟩
-  bind (mono (bind (delta (mono x) ds) id)) (tailDelta ∙ tailDelta)
-  ≡⟨ refl ⟩
-  bind (mono (deltaAppend (headDelta (mono x)) (bind ds tailDelta))) (tailDelta ∙ tailDelta)
-  ≡⟨ refl ⟩
-  bind (mono (deltaAppend (mono x) (bind ds tailDelta))) (tailDelta ∙ tailDelta)
-  ≡⟨ refl ⟩
-  bind (mono (delta x (bind ds tailDelta))) (tailDelta ∙ tailDelta)
-  ≡⟨ refl ⟩
-  (tailDelta ∙ tailDelta) (delta x (bind ds tailDelta))
-  ≡⟨ refl ⟩
-  tailDelta (bind ds tailDelta)
-  ≡⟨ monad-law-1-3 ds ⟩
-  bind (tailDelta ds) (tailDelta ∙ tailDelta)
-  ≡⟨ refl ⟩
-  bind ((tailDelta ∙ tailDelta) (delta (mono x) ds)) (tailDelta ∙ tailDelta)
-  ≡⟨ refl ⟩
-  bind (bind (mono (delta (mono x) ds)) (tailDelta ∙ tailDelta)) (tailDelta ∙ tailDelta)
-  ≡⟨ refl ⟩
-  bind (bind (headDelta (tailDelta (mono (delta (mono x) ds)))) (tailDelta ∙ tailDelta)) (tailDelta ∙ tailDelta)
-  ≡⟨ refl ⟩
-  bind (bind (mono (delta (mono x) ds)) (tailDelta ∙ tailDelta)) (tailDelta ∙ tailDelta)
-  ∎
-monad-law-1-sub-sub (mono (delta (delta x (mono x₁)) ds)) = begin
-  bind (fmap mu (mono (delta (delta x (mono x₁)) ds))) (tailDelta ∙ tailDelta)
-  ≡⟨ refl ⟩
-  bind (mono (mu (delta (delta x (mono x₁)) ds))) (tailDelta ∙ tailDelta)
-  ≡⟨ refl ⟩
-  (tailDelta ∙ tailDelta) (mu (delta (delta x (mono x₁)) ds))
-  ≡⟨ refl ⟩
-  (tailDelta ∙ tailDelta) (bind (delta (delta x (mono x₁)) ds) id)
-  ≡⟨ refl ⟩
-  (tailDelta ∙ tailDelta) (deltaAppend (headDelta (delta x (mono x₁))) (bind ds (tailDelta ∙ id)))
-  ≡⟨ refl ⟩
-  (tailDelta ∙ tailDelta) (deltaAppend (mono x) (bind ds (tailDelta ∙ id)))
-  ≡⟨ refl ⟩
-  (tailDelta ∙ tailDelta) (delta x (bind ds (tailDelta ∙ id)))
-  ≡⟨ refl ⟩
-  tailDelta (bind ds (tailDelta ∙ id))
-  ≡⟨ monad-law-1-3 ds ⟩
-  bind (tailDelta ds) (tailDelta ∙ tailDelta)
-  ≡⟨ refl ⟩
-  bind ((tailDelta ∙ tailDelta) (delta (delta x (mono x₁)) ds)) (tailDelta ∙ tailDelta)
-  ≡⟨ refl ⟩
-  bind (bind (mono (delta (delta x (mono x₁)) ds))  (tailDelta ∙ tailDelta)) (tailDelta ∙ tailDelta)
-  ∎
-monad-law-1-sub-sub (mono (delta (delta x (delta xx d)) ds)) = begin
-  bind (fmap mu (mono (delta (delta x (delta xx d)) ds))) (tailDelta ∙ tailDelta)
-  ≡⟨ refl ⟩
-  bind (mono (mu (delta (delta x (delta xx d)) ds))) (tailDelta ∙ tailDelta)
-  ≡⟨ refl ⟩
-  (tailDelta ∙ tailDelta) (mu (delta (delta x (delta xx d)) ds))
-  ≡⟨ refl ⟩
-  (tailDelta ∙ tailDelta) (bind (delta (delta x (delta xx d)) ds) id)
-  ≡⟨ refl ⟩
-  (tailDelta ∙ tailDelta) (deltaAppend (headDelta (delta x (delta xx d))) (bind ds tailDelta))
-  ≡⟨ refl ⟩
-  (tailDelta ∙ tailDelta) (deltaAppend (mono x) (bind ds tailDelta))
-  ≡⟨ refl ⟩
-  (tailDelta ∙ tailDelta) (delta x (bind ds tailDelta))
-  ≡⟨ refl ⟩
-  tailDelta (bind ds tailDelta)
-  ≡⟨ monad-law-1-3 ds ⟩
-  bind (tailDelta ds) (tailDelta ∙ tailDelta)
-  ≡⟨ refl ⟩
-  bind ((tailDelta ∙ tailDelta) (delta (delta x (delta xx d)) ds)) (tailDelta ∙ tailDelta)
-  ≡⟨ refl ⟩
-  bind (bind (mono (delta (delta x (delta xx d)) ds)) (tailDelta ∙ tailDelta)) (tailDelta ∙ tailDelta)
-  ∎
-monad-law-1-sub-sub (delta (mono (mono x)) ds) = begin
-  bind (fmap mu (delta (mono (mono x)) ds)) (tailDelta ∙ tailDelta)
-  ≡⟨ refl ⟩
-  bind (delta (mu (mono (mono x))) (fmap mu ds)) (tailDelta ∙ tailDelta)
-  ≡⟨ refl ⟩
-  bind (delta (mono x) (fmap mu ds)) (tailDelta ∙ tailDelta)
-  ≡⟨ refl ⟩
-  deltaAppend (headDelta ((tailDelta ∙ tailDelta) (mono x))) (bind (fmap mu ds) (tailDelta ∙ (tailDelta ∙ tailDelta)))
-  ≡⟨ refl ⟩
-  deltaAppend ((tailDelta ∙ tailDelta) (mono x)) (bind (fmap mu ds) (tailDelta ∙ (tailDelta ∙ tailDelta)))
-  ≡⟨ refl ⟩
-  deltaAppend (mono x) (bind (fmap mu ds) (tailDelta ∙ (tailDelta ∙ tailDelta)))
-  ≡⟨ refl ⟩
-  delta x (bind (fmap mu ds) (tailDelta ∙ (tailDelta ∙ tailDelta)))
-  ≡⟨ monad-law-1-4 x ds ⟩ -- ?
-  bind (delta (mono x) (bind ds ((tailDelta ∙ tailDelta ) ∙ tailDelta))) (tailDelta ∙ tailDelta)
-  ≡⟨ refl ⟩
-  bind (delta (tailDelta (mono x)) (bind ds (tailDelta ∙ (tailDelta ∙ tailDelta)))) (tailDelta ∙ tailDelta)
-  ≡⟨ refl ⟩
-  bind (deltaAppend (mono (mono x)) (bind ds (tailDelta ∙ (tailDelta ∙ tailDelta)))) (tailDelta ∙ tailDelta)
-  ≡⟨ refl ⟩
-  bind (deltaAppend (headDelta ((tailDelta ∙ tailDelta) (mono (mono x)))) (bind ds (tailDelta ∙ (tailDelta ∙ tailDelta)))) (tailDelta ∙ tailDelta)
-  ≡⟨ refl ⟩
-  bind (bind (delta (mono (mono x)) ds) (tailDelta ∙ tailDelta)) (tailDelta ∙ tailDelta)
-  ∎
-monad-law-1-sub-sub (delta (mono (delta x d)) ds) = {!!}
-monad-law-1-sub-sub (delta (delta d d₁) ds) = {!!}
-
-
-monad-law-1-sub : {l : Level} {A : Set l} -> (x : Delta (Delta A)) -> (d : Delta (Delta (Delta A))) ->
-  deltaAppend (headDelta (mu x)) (bind (fmap mu d) tailDelta) ≡ mu (deltaAppend (headDelta x) (bind d tailDelta))
-monad-law-1-sub (mono (mono _)) (mono (mono _)) = refl
-monad-law-1-sub (mono (mono _)) (mono (delta (mono _) _)) = refl
-monad-law-1-sub (mono (mono _)) (mono (delta (delta _ _) _)) = refl
-monad-law-1-sub (mono (mono x)) (delta (mono (mono xx)) d) = begin
-  deltaAppend (headDelta (mu (mono (mono x)))) (bind (fmap mu (delta (mono (mono xx)) d)) tailDelta)
-  ≡⟨ refl ⟩
-  deltaAppend (headDelta (mu (mono (mono x)))) (bind (delta (mu (mono (mono xx))) (fmap mu d)) tailDelta)
-  ≡⟨ refl ⟩
-  deltaAppend (headDelta (bind (mono (mono x)) id)) (bind (delta (mu (mono (mono xx))) (fmap mu d)) tailDelta)
-  ≡⟨ refl ⟩
-  deltaAppend (headDelta (mono x)) (bind (delta (mu (mono (mono xx))) (fmap mu d)) tailDelta)
-  ≡⟨ refl ⟩
-  deltaAppend (headDelta (mono x)) (bind (delta (mono xx) (fmap mu d)) tailDelta)
-  ≡⟨ refl ⟩
-  deltaAppend (mono x) (bind (delta (mono xx) (fmap mu d)) tailDelta)
-  ≡⟨ refl ⟩
-  deltaAppend (mono x) (bind (delta (mono xx) (fmap mu d)) tailDelta)
-  ≡⟨ refl ⟩
-  deltaAppend (mono x) (deltaAppend (tailDelta (mono xx)) (bind (fmap mu d) (tailDelta ∙  tailDelta)))
-  ≡⟨ refl ⟩
-  deltaAppend (mono x) (deltaAppend (mono xx) (bind (fmap mu d) (tailDelta ∙  tailDelta)))
-  ≡⟨ refl ⟩
-  deltaAppend (mono x) (deltaAppend (mu (mono (mono xx))) (bind (fmap mu d) (tailDelta ∙  tailDelta)))
-  ≡⟨ refl ⟩
-  deltaAppend (mono x) (deltaAppend (mono xx) (bind (fmap mu d) (tailDelta ∙  tailDelta)))
-  ≡⟨ refl ⟩
-  delta x (deltaAppend (mono xx) (bind (fmap mu d) (tailDelta ∙  tailDelta)))
-  ≡⟨ refl ⟩
-  delta x (delta xx (bind (fmap mu d) (tailDelta ∙  tailDelta)))
-  ≡⟨ cong (\d -> (delta x (delta xx d))) (monad-law-1-sub-sub d) ⟩ -- ???
-  delta x (delta xx (bind (bind d (tailDelta ∙ tailDelta)) (tailDelta ∙ tailDelta)))
-  ≡⟨ refl ⟩
-  delta x ((deltaAppend (mono xx) (bind (bind d (tailDelta ∙ tailDelta)) (tailDelta ∙ tailDelta))))
-  ≡⟨ refl ⟩
-  delta x ((deltaAppend (tailDelta (mono xx)) (bind (bind d (tailDelta ∙ tailDelta)) (tailDelta ∙ tailDelta))))
-  ≡⟨ refl ⟩
-  delta x (bind (delta (mono xx) (bind d (tailDelta ∙ tailDelta))) tailDelta)
-  ≡⟨ refl ⟩
-  delta x (bind (deltaAppend (mono (mono xx)) (bind d (tailDelta ∙ tailDelta))) tailDelta)
-  ≡⟨ refl ⟩
-  delta x (bind (deltaAppend (headDelta (tailDelta (mono (mono xx)))) (bind d (tailDelta ∙ tailDelta))) tailDelta)
-  ≡⟨ refl ⟩
-  delta x (bind (bind (delta (mono (mono xx)) d) tailDelta) tailDelta)
-  ≡⟨ refl ⟩
-  deltaAppend (mono x) (bind (bind (delta (mono (mono xx)) d) tailDelta) tailDelta)
-  ≡⟨ refl ⟩
-  bind (delta (mono x) (bind (delta (mono (mono xx)) d) tailDelta)) id
-  ≡⟨ refl ⟩
-  mu (delta (mono x) (bind (delta (mono (mono xx)) d) tailDelta))
-  ≡⟨ refl ⟩
-  mu (deltaAppend (mono (mono x)) (bind (delta (mono (mono xx)) d) tailDelta))
-  ≡⟨ refl ⟩
-  mu (deltaAppend (headDelta (mono (mono x))) (bind (delta (mono (mono xx)) d) tailDelta))
- ∎
-monad-law-1-sub (mono (mono x)) (delta (mono (delta x₁ d)) d₁) = {!!}
-monad-law-1-sub (mono (mono x)) (delta (delta d d₁) d₂) = {!!}
-monad-law-1-sub (mono (delta x x₁)) d = {!!}
-monad-law-1-sub (delta x x₁) d = {!!}
+monad-law-1-1 (mono (delta (delta x d) ds)) = {!!}
+monad-law-1-1 (delta d ds) = {!!}
 
 -- monad-law-1 : join . fmap join = join . join
 monad-law-1 : {l : Level} {A : Set l} -> (d : Delta (Delta (Delta A))) -> ((mu ∙ (fmap mu)) d) ≡ ((mu ∙ mu) d)
 monad-law-1 (mono d)    = refl
-monad-law-1 (delta x d) = begin
-  (mu ∙ (fmap mu)) (delta x d)
+monad-law-1 (delta (mono x) d)     = begin
+  (mu ∙ fmap mu) (delta (mono x) d)
   ≡⟨ refl ⟩
-  mu (fmap mu (delta x d))
+  mu (fmap mu (delta (mono x) d))
   ≡⟨ refl ⟩
-  mu (delta (mu x) (fmap mu d))
+  mu (delta (mu (mono x)) (fmap mu d))
   ≡⟨ refl ⟩
-  bind (delta (mu x) (fmap mu d)) id
+  mu (delta x (fmap mu d))
+  ≡⟨ cong (\d -> mu (delta x d)) (monad-law-1-1 d) ⟩ -- ? 
+  mu (delta x (bind d tailDelta))
   ≡⟨ refl ⟩
-  deltaAppend (headDelta (mu x)) (bind (fmap mu d) tailDelta)
-  ≡⟨ monad-law-1-sub x d ⟩
-  mu (deltaAppend (headDelta x) (bind d tailDelta))
+  mu (deltaAppend (headDelta (mono x)) (bind d tailDelta))
   ≡⟨ refl ⟩
-  mu (bind (delta x d) id)
-  ≡⟨ refl ⟩
-  mu (mu (delta x d))
+  mu (mu (delta (mono x) d))
   ≡⟨ refl ⟩
-  (mu ∙ mu) (delta x d)
+  (mu ∙ mu) (delta (mono x) d)
   ∎
-
--- split d
-{-
-monad-law-1 (delta x (mono d)) = begin
-
-  (mu ∙ fmap mu) (delta x (mono d))
+monad-law-1 (delta (delta (mono x) xs) d) = begin
+  (mu ∙ fmap mu) (delta (delta (mono x) xs) d)
+  ≡⟨ refl ⟩
+  mu (fmap mu (delta (delta (mono x) xs) d))
+  ≡⟨ refl ⟩
+  mu (delta (mu (delta (mono x) xs)) (fmap mu d))
+  ≡⟨ refl ⟩
+  mu (delta (deltaAppend (headDelta (mono x)) (bind xs tailDelta)) (fmap mu d))
   ≡⟨ refl ⟩
-  mu (fmap mu (delta x (mono d)))
+  mu (delta (delta x (bind xs tailDelta)) (fmap mu d))
   ≡⟨ refl ⟩
-  mu (delta (mu x) (mono (mu d)))
+  deltaAppend (headDelta (delta x (bind xs tailDelta))) (bind (fmap mu d) tailDelta)
   ≡⟨ refl ⟩
-  bind (delta (mu x) (mono (mu d))) id
+  delta x (bind (fmap mu d) tailDelta)
+  ≡⟨ cong (\d -> delta x (bind d tailDelta)) (monad-law-1-1 d) ⟩
+  delta x (bind (bind d tailDelta) tailDelta)
   ≡⟨ refl ⟩
-  deltaAppend (headDelta (mu x)) (bind (mono (mu d)) tailDelta)
+  deltaAppend (headDelta (mono x)) (bind (bind d tailDelta) tailDelta)
   ≡⟨ refl ⟩
-  deltaAppend (headDelta (mu x)) (tailDelta (mu d))
-  ≡⟨ {!!} ⟩
-  mu (deltaAppend (headDelta x) (tailDelta d))
+  mu (delta (mono x) (bind d tailDelta))
   ≡⟨ refl ⟩
-  mu (deltaAppend (headDelta x) (tailDelta (id d)))
-  ≡⟨ refl ⟩
-  mu (deltaAppend (headDelta x) ((tailDelta ∙ id) d))
+  mu (deltaAppend (mono (mono x)) (bind d tailDelta))
   ≡⟨ refl ⟩
-  mu (deltaAppend (headDelta x) (bind  (mono d) (tailDelta ∙ id)))
-  ≡⟨  refl ⟩
-  mu (bind (delta x (mono d)) id)
+  mu (deltaAppend (headDelta (delta (mono x) xs)) (bind d tailDelta))
   ≡⟨ refl ⟩
-  mu (mu (delta x (mono d)))
+  mu (mu (delta (delta (mono x) xs) d))
   ≡⟨ refl ⟩
-  (mu ∙ mu) (delta x (mono d))
+  (mu ∙ mu) (delta (delta (mono x) xs) d)
   ∎
-monad-law-1 (delta x (delta d ds)) = begin
-  (mu ∙ fmap mu) (delta x (delta d ds))
+monad-law-1 (delta (delta (delta x d) xs) ds) = begin
+  (mu ∙ fmap mu) (delta (delta (delta x d) xs) ds)
+  ≡⟨ refl ⟩
+  mu (fmap mu (delta (delta (delta x d) xs) ds))
   ≡⟨ refl ⟩
-  mu (fmap mu (delta x (delta d ds)))
+  mu (delta (mu (delta (delta x d) xs)) (fmap mu ds))
+  ≡⟨ refl ⟩
+  mu (delta (deltaAppend (headDelta (delta x d)) (bind  xs tailDelta)) (fmap mu ds))
   ≡⟨ refl ⟩
-  mu (delta (mu x) (delta (mu d) (fmap mu ds)))
+  mu (delta (delta x (bind  xs tailDelta)) (fmap mu ds))
   ≡⟨ refl ⟩
-  bind (delta (mu x) (delta (mu d) (fmap mu ds))) id
+  deltaAppend (headDelta (delta x (bind  xs tailDelta))) (bind (fmap mu ds) tailDelta)
   ≡⟨ refl ⟩
-  deltaAppend (headDelta (mu x)) (bind (delta (mu d) (fmap mu ds)) tailDelta)
+  delta x (bind (fmap mu ds) tailDelta)
+  ≡⟨ cong (\d -> delta x (bind d tailDelta)) (monad-law-1-1 ds) ⟩
+  delta x (bind (bind ds tailDelta) tailDelta)
+  ≡⟨ refl ⟩
+  deltaAppend (headDelta (delta x d)) (bind (bind ds tailDelta) tailDelta)
   ≡⟨ refl ⟩
-  deltaAppend (headDelta (mu x)) (deltaAppend (headDelta (tailDelta (mu d))) (bind (fmap mu ds) (tailDelta ∙ tailDelta)))
-
-  ≡⟨ {!!} ⟩
-  (mu ∙ mu) (delta x (delta d ds))
+  mu (delta (delta x d) (bind ds tailDelta))
+  ≡⟨ refl ⟩
+  mu (deltaAppend (headDelta (delta (delta x d) xs)) (bind ds tailDelta))
+  ≡⟨ refl ⟩
+  (mu ∙ mu) (delta (delta (delta x d) xs) ds)
   ∎
--}
-
 
 {-
 monad-law-1 : {l : Level} {A : Set l} -> (d : Delta (Delta (Delta A))) -> ((mu ∙ (fmap mu)) d) ≡ ((mu ∙ mu) d)
@@ -472,7 +251,7 @@
 monad-law-1 (delta x (delta xx d)) = {!!}
 
 monad-law-1 (delta x d) = begin
-   (mu ∙ fmap mu) (delta x d) 
+   (mu ∙ fmap mu) (delta x d)
    ≡⟨ refl ⟩
    mu ((fmap mu) (delta x d))
    ≡⟨ refl ⟩