Mercurial > hg > Members > atton > delta_monad
diff agda/deltaM/monad.agda @ 131:d205ff1e406f InfiniteDeltaWithMonad
Cleanup proofs
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 03 Feb 2015 12:57:13 +0900 |
| parents | ac45d065cbf2 |
| children | 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))) } - - - -