Mercurial > hg > Members > atton > delta_monad
diff agda/delta/functor.agda @ 112:0a3b6cb91a05
Prove left-unity-law for DeltaM
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 30 Jan 2015 21:57:31 +0900 |
parents | e6499a50ccbd |
children | 47f144540d51 |
line wrap: on
line diff
--- a/agda/delta/functor.agda Thu Jan 29 11:42:22 2015 +0900 +++ b/agda/delta/functor.agda Fri Jan 30 21:57:31 2015 +0900 @@ -1,5 +1,6 @@ open import Level open import Relation.Binary.PropositionalEquality +open ≡-Reasoning open import basic open import delta @@ -22,22 +23,21 @@ 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} - - -open ≡-Reasoning -delta-fmap-equiv : {l : Level} {A B : Set l} {n : Nat} - (f g : A -> B) (eq : f ≡ g) (d : Delta A (S n)) -> - delta-fmap f d ≡ delta-fmap g d -delta-fmap-equiv f g eq (mono x) = begin - mono (f x) ≡⟨ cong (\h -> (mono (h x))) eq ⟩ - mono (g x) ∎ -delta-fmap-equiv f g eq (delta x d) = begin - delta (f x) (delta-fmap f d) ≡⟨ cong (\h -> (delta (h x) (delta-fmap f d))) eq ⟩ - delta (g x) (delta-fmap f d) ≡⟨ cong (\fx -> (delta (g x) fx)) (delta-fmap-equiv f g eq d) ⟩ - delta (g x) (delta-fmap g d) ∎ + covariant = \f g -> functor-law-2 g f; + fmap-equiv = delta-fmap-equiv }