Mercurial > hg > Members > atton > delta_monad

changeset 136:b6dcbe8617a9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Delete unnecessary lines
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sun, 15 Feb 2015 10:15:10 +0900
parents bb0b2fb49a93
children 2bf1fa6d2006
files agda/delta/monad.agda
diffstat 1 files changed, 0 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/agda/delta/monad.agda	Sat Feb 07 14:43:20 2015 +0900
+++ b/agda/delta/monad.agda	Sun Feb 15 10:15:10 2015 +0900
@@ -10,11 +10,6 @@
 
 module delta.monad where
 
-tailDelta-is-nt : {l : Level} {A B : Set l} {n : Nat}
-                  (f : A -> B) -> (d : Delta A (S (S n))) ->
-                  (tailDelta {n = n} ∙ (delta-fmap f)) d ≡ ((delta-fmap f) ∙ tailDelta {n = n}) d
-tailDelta-is-nt f (delta x d) = refl
-
 
 tailDelta-to-tail-nt : {l : Level} {A B : Set l} (n m  : Nat)
                        (f : A -> B) (d : Delta (Delta A (S (S m))) (S n)) ->
@@ -40,7 +35,6 @@
 delta-eta-is-nt : {l : Level} {A B : Set l} -> {n : Nat}
                   (f : A -> B) -> (x : A) -> (delta-eta {n = n} ∙ f) x ≡ delta-fmap f (delta-eta x)
 delta-eta-is-nt {n = O}   f x = refl
-delta-eta-is-nt {n = S O} f x = refl
 delta-eta-is-nt {n = S n} f x = begin
   (delta-eta ∙ f) x                        ≡⟨ refl ⟩
   delta-eta (f x)                          ≡⟨ refl ⟩