Cleanup proofs
author Yasutaka Higa Tue, 03 Feb 2015 12:57:13 +0900 ac45d065cbf2 575de2e38385
line wrap: on
line diff
```--- a/agda/deltaM/monad.agda	Tue Feb 03 12:46:20 2015 +0900
+++ b/agda/deltaM/monad.agda	Tue Feb 03 12:57:13 2015 +0900
@@ -32,6 +32,7 @@
headDeltaM-with-f {n = O} f   (deltaM (mono x))    = refl
headDeltaM-with-f {n = S n} f (deltaM (delta x d)) = refl

+
tailDeltaM-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) -> (d : (DeltaM M A (S (S n)))) ->
@@ -39,21 +40,6 @@
tailDeltaM-with-f {n = O} f (deltaM (delta x d))   = refl
tailDeltaM-with-f {n = S n} f (deltaM (delta x d)) = refl

-headDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat}
-                             {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
-                             (x : DeltaM M A (S n)) ->
-                             ((headDeltaM {n = n} {M = M}) ∙ deltaM-eta) x ≡ eta M x
-headDeltaM-with-deltaM-eta {n = O} (deltaM (mono x))      = refl
-headDeltaM-with-deltaM-eta {n = S n} (deltaM (delta x d)) = refl
-
-
-fmap-tailDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat}
-                                  {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
-                                  (d : DeltaM M A (S n)) ->
-        deltaM-fmap ((tailDeltaM {n = n} {M = M} ) ∙ deltaM-eta) d ≡ deltaM-fmap (deltaM-eta) d
-fmap-tailDeltaM-with-deltaM-eta {n = O}   d = refl
-fmap-tailDeltaM-with-deltaM-eta {n = S n} d = refl
-

fmap-headDeltaM-with-deltaM-mu : {l : Level} {A : Set l} {n : Nat}
@@ -455,7 +441,3 @@
; left-unity-law  = deltaM-left-unity-law
; right-unity-law = (\x -> (sym (deltaM-right-unity-law x)))
}
-
-
-
-```