changeset 130:ac45d065cbf2

Prove all Monad-laws for Delta with Monad
author Yasutaka Higa Tue, 03 Feb 2015 12:46:20 +0900 d57c88171f38 d205ff1e406f agda/deltaM/monad.agda 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)))
}

--}
+```