Mercurial > hg > Members > atton > delta_monad
diff agda/delta/functor.agda @ 126:5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 03 Feb 2015 11:45:33 +0900 |
parents | 47f144540d51 |
children | d205ff1e406f |
line wrap: on
line diff
--- a/agda/delta/functor.agda Mon Feb 02 14:09:30 2015 +0900 +++ b/agda/delta/functor.agda Tue Feb 03 11:45:33 2015 +0900 @@ -24,9 +24,24 @@ 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 {l} {A} {B} {O} {f} {g} eq (mono x) = begin + mono (f x) ≡⟨ cong mono (eq x) ⟩ + mono (g x) + ∎ +delta-fmap-equiv {l} {A} {B} {S n} {f} {g} eq (delta x d) = begin + delta (f x) (delta-fmap f d) ≡⟨ cong (\de -> delta de (delta-fmap f d)) (eq x) ⟩ + delta (g x) (delta-fmap f d) ≡⟨ cong (\de -> delta (g x) de) (delta-fmap-equiv 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 - } +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 + }