Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM/functor.agda @ 126:5902b2a24abf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 ee7f5162ec1f
children d205ff1e406f
comparison
equal deleted inserted replaced
125:6dcc68ef8f96 126:5902b2a24abf
73 appendDeltaM (deltaM ((((delta-fmap (fmap F f)) ∙ (delta-fmap (fmap F g)))) (mono x))) (((deltaM-fmap f) ∙ (deltaM-fmap g)) (deltaM d)) 73 appendDeltaM (deltaM ((((delta-fmap (fmap F f)) ∙ (delta-fmap (fmap F g)))) (mono x))) (((deltaM-fmap f) ∙ (deltaM-fmap g)) (deltaM d))
74 ≡⟨ refl ⟩ 74 ≡⟨ refl ⟩
75 (deltaM-fmap f ∙ deltaM-fmap g) (deltaM (delta x d)) 75 (deltaM-fmap f ∙ deltaM-fmap g) (deltaM (delta x d))
76 ∎ 76 ∎
77 77
78 deltaM-fmap-equiv : {l : Level} {A B : Set l} {n : Nat}
79 {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
80 {f g : A -> B}
81 (eq : (x : A) -> f x ≡ g x) -> (d : DeltaM M A (S n)) ->
82 deltaM-fmap f d ≡ deltaM-fmap g d
83 deltaM-fmap-equiv {l} {A} {B} {O} {T} {F} {M} {f} {g} eq (deltaM (mono x)) = begin
84 deltaM-fmap f (deltaM (mono x)) ≡⟨ refl ⟩
85 deltaM (mono (fmap F f x)) ≡⟨ cong (\de -> deltaM (mono de)) (fmap-equiv F eq x) ⟩
86 deltaM (mono (fmap F g x)) ≡⟨ refl ⟩
87 deltaM-fmap g (deltaM (mono x))
88 ∎
89 deltaM-fmap-equiv {l} {A} {B} {S n} {T} {F} {M} {f} {g} eq (deltaM (delta x d)) = begin
90 deltaM-fmap f (deltaM (delta x d)) ≡⟨ refl ⟩
91 deltaM (delta (fmap F f x) (delta-fmap (fmap F f) d)) ≡⟨ cong (\de -> deltaM (delta de (delta-fmap (fmap F f) d))) (fmap-equiv F eq x) ⟩
92 deltaM (delta (fmap F g x) (delta-fmap (fmap F f) d)) ≡⟨ cong (\de -> deltaM (delta (fmap F g x) de)) (delta-fmap-equiv (fmap-equiv F eq) d) ⟩
93 deltaM (delta (fmap F g x) (delta-fmap (fmap F g) d)) ≡⟨ refl ⟩
94 deltaM-fmap g (deltaM (delta x d))
95 ∎
96
78 97
79 98
80 deltaM-is-functor : {l : Level} {n : Nat} 99 deltaM-is-functor : {l : Level} {n : Nat}
81 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} -> 100 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
82 Functor {l} (\A -> DeltaM M A (S n)) 101 Functor {l} (\A -> DeltaM M A (S n))
83 deltaM-is-functor {F = F} = record { fmap = deltaM-fmap 102 deltaM-is-functor {F = F} = record { fmap = deltaM-fmap
84 ; preserve-id = deltaM-preserve-id {F = F} 103 ; preserve-id = deltaM-preserve-id {F = F}
85 ; covariant = (\f g -> deltaM-covariant {F = F} g f) 104 ; covariant = (\f g -> deltaM-covariant {F = F} g f)
105 ; fmap-equiv = deltaM-fmap-equiv
86 } 106 }
87 107
88 108