### changeset 96:dfe8c67390bd

Unify Levels in delta
author Yasutaka Higa Tue, 20 Jan 2015 16:25:53 +0900 cf372fbcebd8 f26a954cd068 agda/delta.agda agda/delta/monad.agda 2 files changed, 22 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
```--- 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```
```--- 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 (delta _ _) = refl

monad-law-1-3 : {l : Level} {A : Set l} -> (n : Nat) -> (d : Delta (Delta (Delta A))) ->
@@ -265,7 +265,7 @@

-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 @@

+
{-
+
-- 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-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-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```