Mercurial > hg > Members > atton > delta_monad

diff agda/deltaM/functor.agda @ 103:a271f3ff1922

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Delte type dependencie in Monad record for escape implicit type conflict
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 26 Jan 2015 14:08:46 +0900
parents 8d92ed54a94f
children ebd0d6e2772c
line wrap: on
line diff
--- a/agda/deltaM/functor.agda	Sun Jan 25 12:16:34 2015 +0900
+++ b/agda/deltaM/functor.agda	Mon Jan 26 14:08:46 2015 +0900
@@ -15,7 +15,7 @@
 deltaM-preserve-id :  {l : Level} {A : Set l}
                       {M : {l' : Level} -> Set l' -> Set l'}
                       (functorM : {l' : Level} -> Functor {l'} M)
-                      {monadM   : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
+                      {monadM   : {l' : Level} -> Monad {l'} M functorM}
                       -> (d : DeltaM M {functorM} {monadM} A) -> deltaM-fmap id d ≡ id d
 deltaM-preserve-id functorM (deltaM (mono x))  = begin
   deltaM-fmap id (deltaM (mono x))                           ≡⟨ refl ⟩
@@ -45,7 +45,7 @@
 deltaM-covariant : {l : Level} {A B C : Set l} ->
                    {M : {l' : Level} -> Set l' -> Set l'}
                    (functorM : {l' : Level} -> Functor {l'} M)
-                   {monadM   : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
+                   {monadM   : {l' : Level} -> Monad {l'}  M functorM}
                    (f : B -> C) -> (g : A -> B) -> (d : DeltaM M {functorM} {monadM} A) ->
                    (deltaM-fmap (f ∙ g)) d ≡ ((deltaM-fmap f) ∙ (deltaM-fmap g)) d
 deltaM-covariant functorM f g (deltaM (mono x))    = begin
@@ -81,7 +81,7 @@
 
 deltaM-is-functor : {l : Level} {M : {l' : Level} -> Set l' -> Set l'}
                                 {functorM : {l' : Level} -> Functor {l'} M }
-                                {monadM   : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
+                                {monadM   : {l' : Level} -> Monad {l'} M functorM}
                     -> Functor {l} (DeltaM M {functorM} {monadM}) 
 deltaM-is-functor {_} {_} {functorM} = record { fmap        = deltaM-fmap ;
                              preserve-id  = deltaM-preserve-id functorM ;