diff agda/delta/monad.agda @ 104:ebd0d6e2772c

Trying redenition Delta with length constraints
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 26 Jan 2015 23:00:05 +0900
parents a271f3ff1922
children e6499a50ccbd
line wrap: on
line diff
--- a/agda/delta/monad.agda	Mon Jan 26 14:08:46 2015 +0900
+++ b/agda/delta/monad.agda	Mon Jan 26 23:00:05 2015 +0900
@@ -3,6 +3,7 @@
 open import delta.functor
 open import nat
 open import laws
+open import revision
 
 
 open import Level
@@ -13,6 +14,7 @@
 
 
 -- Monad-laws (Category)
+{-
 
 monad-law-1-5 : {l : Level} {A : Set l} -> (m : Nat) (n : Nat) -> (ds : Delta (Delta A)) ->
   n-tail n (delta-bind ds (n-tail m))  ≡ delta-bind (n-tail n ds) (n-tail (m + n))
@@ -322,14 +324,25 @@
   delta-fmap f (delta-mu (delta (delta x d) ds))                                              ≡⟨ refl ⟩
   (delta-fmap f ∙ delta-mu) (delta (delta x d) ds) ∎
 
-delta-is-monad : {l : Level} -> Monad {l} Delta delta-is-functor
+-}
+-- monad-law-1 : join . delta-fmap join = join . join
+monad-law-1 : {l : Level} {A : Set l} {a : Rev} -> (d : Delta (Delta (Delta A a) a) a) ->
+            ((delta-mu ∙ (delta-fmap delta-mu)) d) ≡ ((delta-mu ∙ delta-mu) d)
+monad-law-1 (mono d)     = refl
+monad-law-1 (delta d ds) = {!!}
+
+delta-is-monad : {l : Level} {v : Rev} -> Monad {l} (\A -> Delta A v)  delta-is-functor
+
+
 delta-is-monad = record { eta    = delta-eta;
                           mu     = delta-mu;
                           return = delta-eta;
                           bind   = delta-bind;
-                          association-law = monad-law-1;
-                          left-unity-law  = monad-law-2;
-                          right-unity-law = monad-law-2' }
+                          association-law = monad-law-1 }
+--                          left-unity-law  = monad-law-2;
+--                          right-unity-law = monad-law-2' }
+
+