Mercurial > hg > Members > atton > delta_monad
diff agda/deltaM/functor.agda @ 104:ebd0d6e2772c
Trying redenition Delta with length constraints
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 26 Jan 2015 23:00:05 +0900 |
| parents | a271f3ff1922 |
| children | cd058dd89864 |
line wrap: on
line diff
--- a/agda/deltaM/functor.agda Mon Jan 26 14:08:46 2015 +0900 +++ b/agda/deltaM/functor.agda Mon Jan 26 23:00:05 2015 +0900 @@ -6,17 +6,19 @@ open import delta open import delta.functor open import deltaM +open import nat +open import revision open import laws open Functor module deltaM.functor where -deltaM-preserve-id : {l : Level} {A : Set l} +deltaM-preserve-id : {l : Level} {A : Set l} {n : Rev} {M : {l' : Level} -> Set l' -> Set l'} (functorM : {l' : Level} -> Functor {l'} M) {monadM : {l' : Level} -> Monad {l'} M functorM} - -> (d : DeltaM M {functorM} {monadM} A) -> deltaM-fmap id d ≡ id d + -> (d : DeltaM M {functorM} {monadM} A n) -> deltaM-fmap id d ≡ id d deltaM-preserve-id functorM (deltaM (mono x)) = begin deltaM-fmap id (deltaM (mono x)) ≡⟨ refl ⟩ deltaM (fmap delta-is-functor (fmap functorM id) (mono x)) ≡⟨ refl ⟩ @@ -42,11 +44,11 @@ ∎ -deltaM-covariant : {l : Level} {A B C : Set l} -> +deltaM-covariant : {l : Level} {A B C : Set l} {n : Rev} -> {M : {l' : Level} -> Set l' -> Set l'} (functorM : {l' : Level} -> Functor {l'} M) {monadM : {l' : Level} -> Monad {l'} M functorM} - (f : B -> C) -> (g : A -> B) -> (d : DeltaM M {functorM} {monadM} A) -> + (f : B -> C) -> (g : A -> B) -> (d : DeltaM M {functorM} {monadM} A n) -> (deltaM-fmap (f ∙ g)) d ≡ ((deltaM-fmap f) ∙ (deltaM-fmap g)) d deltaM-covariant functorM f g (deltaM (mono x)) = begin deltaM-fmap (f ∙ g) (deltaM (mono x)) ≡⟨ refl ⟩ @@ -79,10 +81,11 @@ ∎ -deltaM-is-functor : {l : Level} {M : {l' : Level} -> Set l' -> Set l'} +deltaM-is-functor : {l : Level} {n : Rev} + {M : {l' : Level} -> Set l' -> Set l'} {functorM : {l' : Level} -> Functor {l'} M } {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 ; - covariant = (\f g -> deltaM-covariant functorM g f)} \ No newline at end of file + -> Functor {l} (\A -> DeltaM M {functorM} {monadM} A n) +deltaM-is-functor {_} {_} {_} {functorM} = record { fmap = deltaM-fmap ; + preserve-id = deltaM-preserve-id functorM ; + covariant = (\f g -> deltaM-covariant functorM g f)}