# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1421738753 -32400
# Node ID dfe8c67390bd4a9a7f67cf215729d9ff85d3bee7
# Parent  cf372fbcebd89201d24ee961a7bcbbba98b76be1
Unify Levels in delta

diff -r cf372fbcebd8 -r dfe8c67390bd agda/delta.agda
--- a/agda/delta.agda	Mon Jan 19 17:47:55 2015 +0900
+++ b/agda/delta.agda	Tue Jan 20 16:25:53 2015 +0900
@@ -32,7 +32,7 @@
 
 
 -- Functor
-delta-fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> (Delta A) -> (Delta B)
+delta-fmap : {l : Level} {A B : Set l} -> (A -> B) -> (Delta A) -> (Delta B)
 delta-fmap f (mono x)    = mono  (f x)
 delta-fmap f (delta x d) = delta (f x) (delta-fmap f d)
 
@@ -100,12 +100,12 @@
   tailDelta (mono x)              ≡⟨ refl ⟩
   mono x                          ∎
 
-head-delta-natural-transformation : {l ll : Level} {A : Set l} {B : Set ll}
+head-delta-natural-transformation : {l : Level} {A B : Set l}
   -> (f : A -> B) -> (d : Delta A) -> headDelta (delta-fmap f d) ≡ f (headDelta d)
 head-delta-natural-transformation f (mono x)    = refl
 head-delta-natural-transformation f (delta x d) = refl
 
-n-tail-natural-transformation  : {l ll : Level} {A : Set l} {B : Set ll}
+n-tail-natural-transformation  : {l  : Level} {A B : Set l} 
   -> (n : Nat) -> (f : A -> B) -> (d : Delta A) ->  n-tail n (delta-fmap f d) ≡ delta-fmap f (n-tail n d)
 n-tail-natural-transformation O f d            = refl
 n-tail-natural-transformation (S n) f (mono x) = begin
diff -r cf372fbcebd8 -r dfe8c67390bd agda/delta/monad.agda
--- a/agda/delta/monad.agda	Mon Jan 19 17:47:55 2015 +0900
+++ b/agda/delta/monad.agda	Tue Jan 20 16:25:53 2015 +0900
@@ -128,7 +128,7 @@
   ∎
 
 monad-law-1-2 : {l : Level} {A : Set l} -> (d : Delta (Delta A)) -> headDelta (delta-mu d) ≡ (headDelta (headDelta d))
-monad-law-1-2 (mono _) = refl
+monad-law-1-2 (mono _)    = refl
 monad-law-1-2 (delta _ _) = refl
 
 monad-law-1-3 : {l : Level} {A : Set l} -> (n : Nat) -> (d : Delta (Delta (Delta A))) ->
@@ -265,7 +265,7 @@
 monad-law-3 f x = refl
 
 
-monad-law-4-1 : {l ll : Level} {A : Set l} {B : Set ll} -> (n : Nat) -> (f : A -> B) -> (ds : Delta (Delta A)) ->
+monad-law-4-1 : {l  : Level} {A B : Set l} -> (n : Nat) -> (f : A -> B) -> (ds : Delta (Delta A)) ->
   delta-bind (delta-fmap (delta-fmap f) ds) (n-tail n) ≡ delta-fmap f (delta-bind ds (n-tail n))
 monad-law-4-1 O f (mono d)     = refl
 monad-law-4-1 O f (delta d ds) = begin
@@ -332,28 +332,35 @@
                           right-unity-law = monad-law-2' }
 
 
+
 {-
+
 -- Monad-laws (Haskell)
 -- monad-law-h-1 : return a >>= k  =  k a
-monad-law-h-1 : {l ll : Level} {A : Set l} {B : Set ll} ->
+monad-law-h-1 : {l : Level} {A B : Set l} -> 
                 (a : A) -> (k : A -> (Delta B)) ->
-                (return a >>= k)  ≡ (k a)
+                (delta-return a >>= k)  ≡ (k a)
 monad-law-h-1 a k = refl
 
 
 
 -- monad-law-h-2 : m >>= return  =  m
-monad-law-h-2 : {l : Level}{A : Set l} -> (m : Delta A) -> (m >>= return)  ≡ m
+monad-law-h-2 : {l : Level}{A : Set l} -> (m : Delta A) -> (m >>= delta-return)  ≡ m
 monad-law-h-2 (mono x)    = refl
 monad-law-h-2 (delta x d) = cong (delta x) (monad-law-h-2 d)
 
 
--- monad-law-h-3 : m >>= (\x -> k x >>= h)  =  (m >>= k) >>= h
-monad-law-h-3 : {l ll lll : Level} {A : Set l} {B : Set ll} {C : Set lll} ->
-                (m : Delta A)  -> (k : A -> (Delta B)) -> (h : B -> (Delta C)) ->
-                (m >>= (\x -> k x >>= h)) ≡ ((m >>= k) >>= h)
-monad-law-h-3 (mono x) k h    = refl
-monad-law-h-3 (delta x d) k h = {!!}
 
--}
+-- monad-law-h-3 : m >>= (\x -> f x >>= g)  =  (m >>= f) >>= g
+monad-law-h-3 : {l : Level} {A B C : Set l} -> 
+                (m : Delta A)  -> (f : A -> (Delta B)) -> (g : B -> (Delta C)) ->
+                (delta-bind m (\x -> delta-bind (f x) g)) ≡ (delta-bind (delta-bind m f) g)
+monad-law-h-3 (mono x) f g     = refl
+monad-law-h-3 (delta x d) f g = begin
+  (delta-bind (delta x d) (\x -> delta-bind (f x) g)) ≡⟨ {!!} ⟩
+  (delta-bind (delta-bind (delta x d) f) g) ∎
 
+
+
+
+-}
\ No newline at end of file