Mercurial > hg > Members > atton > delta_monad

diff agda/deltaM/functor.agda @ 131:d205ff1e406f InfiniteDeltaWithMonad

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Cleanup proofs
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 03 Feb 2015 12:57:13 +0900
parents 5902b2a24abf
children
line wrap: on
line diff
--- a/agda/deltaM/functor.agda	Tue Feb 03 12:46:20 2015 +0900
+++ b/agda/deltaM/functor.agda	Tue Feb 03 12:57:13 2015 +0900
@@ -75,7 +75,7 @@
   (deltaM-fmap f ∙ deltaM-fmap g) (deltaM (delta x d))
   ∎
 
-deltaM-fmap-equiv : {l : Level} {A B : Set l} {n : Nat} 
+deltaM-fmap-equiv : {l : Level} {A B : Set l} {n : Nat}
                     {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
                     {f g : A -> B}
                     (eq : (x : A) -> f x ≡ g x) -> (d : DeltaM M A (S n)) ->
@@ -104,5 +104,3 @@
                                    ; covariant    = (\f g -> deltaM-covariant {F = F} g f)
                                    ; fmap-equiv   = deltaM-fmap-equiv
                                    }
-
-