Mercurial > hg > Members > atton > delta_monad

changeset 130:ac45d065cbf2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove all Monad-laws for Delta with Monad
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 03 Feb 2015 12:46:20 +0900
parents d57c88171f38
children d205ff1e406f
files agda/deltaM/monad.agda
diffstat 1 files changed, 13 insertions(+), 23 deletions(-) [+]
line wrap: on
line diff
--- a/agda/deltaM/monad.agda	Tue Feb 03 12:42:28 2015 +0900
+++ b/agda/deltaM/monad.agda	Tue Feb 03 12:46:20 2015 +0900
@@ -27,7 +27,7 @@
 
 headDeltaM-with-f : {l : Level} {A B : Set l} {n : Nat}
                     {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
-                    (f : A -> B) -> (x : (DeltaM M A (S n))) -> 
+                    (f : A -> B) -> (x : (DeltaM M A (S n))) ->
                     ((fmap F f) ∙ headDeltaM) x ≡ (headDeltaM ∙ (deltaM-fmap f)) x
 headDeltaM-with-f {n = O} f   (deltaM (mono x))    = refl
 headDeltaM-with-f {n = S n} f (deltaM (delta x d)) = refl
@@ -74,7 +74,7 @@
 
 
 
-{-
+
 -- main proofs
 
 deltaM-eta-is-nt : {l : Level} {A B : Set l} {n : Nat}
@@ -154,7 +154,7 @@
   ≡⟨ refl ⟩
   deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
                 (unDeltaM {M = M} (deltaM-fmap f (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
-  ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM de))) 
+  ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM de)))
            (deltaM-mu-is-nt {l} {A} {B} {n} {T} {F} {M} f (deltaM-fmap tailDeltaM (deltaM d))) ⟩
   deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
                 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (deltaM-fmap {n = n} f) (deltaM-fmap {n = n} (tailDeltaM {n = n}) (deltaM d))))))
@@ -254,9 +254,9 @@
   deltaM-mu (deltaM-fmap deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩
   deltaM-mu (deltaM (mono (fmap F deltaM-eta x)))      ≡⟨ refl ⟩
   deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F deltaM-eta x)))))))      ≡⟨ refl ⟩
-  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F deltaM-eta x)))) 
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F deltaM-eta x))))
   ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F deltaM-eta headDeltaM x)) ⟩
-  deltaM (mono (mu M (fmap F ((headDeltaM {n = O} {M = M}) ∙ deltaM-eta) x))) 
+  deltaM (mono (mu M (fmap F ((headDeltaM {n = O} {M = M}) ∙ deltaM-eta) x)))
   ≡⟨ refl ⟩
   deltaM (mono (mu M (fmap F (eta M) x)))
   ≡⟨ cong (\de -> deltaM (mono de)) (left-unity-law M x) ⟩
@@ -294,13 +294,6 @@
   deltaM (delta x d)
   ∎
 
--}
-
-postulate deltaM-mu-is-nt : {l : Level} {A B : Set l} {n : Nat}
-                  {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
-                  (f : A -> B) -> (d : DeltaM M (DeltaM M A (S n)) (S n)) ->
-                  deltaM-fmap f (deltaM-mu d) ≡ deltaM-mu (deltaM-fmap (deltaM-fmap f) d)
-
 deltaM-association-law : {l : Level} {A : Set l} {n : Nat}
                          {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
                          (d : DeltaM M (DeltaM M (DeltaM M A (S n)) (S n))  (S n)) ->
@@ -339,8 +332,7 @@
   deltaM-mu (deltaM-mu (deltaM (mono x)))
 
   ∎
-deltaM-association-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = {!!}
-{-
+
 deltaM-association-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin
   deltaM-mu (deltaM-fmap deltaM-mu (deltaM (delta x d)))
   ≡⟨ refl ⟩
@@ -447,25 +439,23 @@
   ≡⟨ refl ⟩
   deltaM-mu (deltaM-mu (deltaM (delta x d)))
   ∎
--}
+
 
-{-
+
 
 deltaM-is-monad : {l : Level} {A : Set l} {n : Nat}
-                              {M : Set l -> Set l}
-                              (functorM : Functor M)
-                              (M   : Monad M functorM) ->
-               Monad {l} (\A -> DeltaM M {functorM} {M} A (S n)) (deltaM-is-functor {l} {n})
-deltaM-is-monad {l} {A} {n} {M} functorM M =
+                  {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
+                  Monad {l} (\A -> DeltaM M A (S n)) (deltaM-is-functor {l} {n})
+deltaM-is-monad {l} {A} {n} {T} {F} {M} =
                 record { mu     = deltaM-mu
                        ; eta    = deltaM-eta
                        ; eta-is-nt = deltaM-eta-is-nt
                        ; mu-is-nt = (\f x -> (sym (deltaM-mu-is-nt f x)))
-                       ; association-law = (deltaM-association-law M functorM M)
+                       ; association-law = deltaM-association-law
                        ; left-unity-law  = deltaM-left-unity-law
                        ; right-unity-law = (\x -> (sym (deltaM-right-unity-law x)))
                        }
 
 
 
--}
+