Mercurial > hg > Members > atton > delta_monad
changeset 113:47f144540d51
Delte trying code
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 30 Jan 2015 21:59:06 +0900 |
| parents | 0a3b6cb91a05 |
| children | 08403eb8db8b |
| files | agda/delta/functor.agda agda/deltaM/functor.agda agda/laws.agda |
| diffstat | 3 files changed, 4 insertions(+), 32 deletions(-) [+] |
line wrap: on
line diff
--- a/agda/delta/functor.agda Fri Jan 30 21:57:31 2015 +0900 +++ b/agda/delta/functor.agda Fri Jan 30 21:59:06 2015 +0900 @@ -23,21 +23,10 @@ functor-law-2 f g (mono x) = refl functor-law-2 f g (delta x d) = cong (delta (f (g x))) (functor-law-2 f g d) -delta-fmap-equiv : {l : Level} {A B : Set l} {n : Nat} - {f g : A -> B} -> (eq : (x : A) -> f x ≡ g x) (d : Delta A (S n)) -> - delta-fmap f d ≡ delta-fmap g d -delta-fmap-equiv {f = f} {g = g} eq (mono x) = begin - mono (f x) ≡⟨ cong (\he -> (mono he)) (eq x) ⟩ - mono (g x) ∎ -delta-fmap-equiv {f = f} {g = g} eq (delta x d) = begin - delta (f x) (delta-fmap f d) ≡⟨ cong (\hx -> (delta hx (delta-fmap f d))) (eq x) ⟩ - delta (g x) (delta-fmap f d) ≡⟨ cong (\fx -> (delta (g x) fx)) (delta-fmap-equiv {f = f} {g = g} eq d) ⟩ - delta (g x) (delta-fmap g d) ∎ - delta-is-functor : {l : Level} {n : Nat} -> Functor {l} (\A -> Delta A (S n)) delta-is-functor = record { fmap = delta-fmap ; preserve-id = functor-law-1; - covariant = \f g -> functor-law-2 g f; - fmap-equiv = delta-fmap-equiv } + covariant = \f g -> functor-law-2 g f + }
--- a/agda/deltaM/functor.agda Fri Jan 30 21:57:31 2015 +0900 +++ b/agda/deltaM/functor.agda Fri Jan 30 21:59:06 2015 +0900 @@ -79,21 +79,7 @@ (deltaM-fmap f ∙ deltaM-fmap g) (deltaM (delta x d)) ∎ -postulate deltaM-fmap-equiv : {l : Level} {A B : Set l} {n : Nat} - {M : Set l -> Set l} - {functorM : Functor M} - {monadM : Monad M functorM} - {f g : A -> B} - (eq : (x : A) -> f x ≡ g x) - (d : DeltaM M {functorM} {monadM} A (S n)) -> - deltaM-fmap f d ≡ deltaM-fmap g d -{- -deltaM-fmap-equiv {n = O} f g eq (deltaM (mono x)) = begin - {!!} ≡⟨ {!!} ⟩ - {!!} - ∎ -deltaM-fmap-equiv {n = S n} f g eq d = {!!} --} + deltaM-is-functor : {l : Level} {n : Nat} {M : Set l -> Set l} @@ -102,6 +88,5 @@ -> Functor {l} (\A -> DeltaM M {functorM} {monadM} A (S n)) deltaM-is-functor {_} {_} {_} {functorM} = record { fmap = deltaM-fmap ; preserve-id = deltaM-preserve-id functorM ; - covariant = (\f g -> deltaM-covariant functorM g f); - fmap-equiv = deltaM-fmap-equiv + covariant = (\f g -> deltaM-covariant functorM g f) }
--- a/agda/laws.agda Fri Jan 30 21:57:31 2015 +0900 +++ b/agda/laws.agda Fri Jan 30 21:59:06 2015 +0900 @@ -11,8 +11,6 @@ preserve-id : {A : Set l} (x : F A) → fmap id x ≡ id x covariant : {A B C : Set l} (f : A -> B) -> (g : B -> C) -> (x : F A) -> fmap (g ∙ f) x ≡ ((fmap g) ∙ (fmap f)) x - field - fmap-equiv : {A B : Set l} {f g : A -> B} -> ((x : A) -> f x ≡ g x) -> (x : F A) -> fmap f x ≡ fmap g x open Functor record NaturalTransformation {l : Level} (F G : {l' : Level} -> Set l' -> Set l')