Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM/functor.agda @ 131:d205ff1e406f InfiniteDeltaWithMonad

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Cleanup proofs
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 03 Feb 2015 12:57:13 +0900
parents 5902b2a24abf
children
comparison
equal deleted inserted replaced
130:ac45d065cbf2 131:d205ff1e406f
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} 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} 79 {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
80 {f g : A -> B} 80 {f g : A -> B}
81 (eq : (x : A) -> f x ≡ g x) -> (d : DeltaM M A (S n)) -> 81 (eq : (x : A) -> f x ≡ g x) -> (d : DeltaM M A (S n)) ->
82 deltaM-fmap f d ≡ deltaM-fmap g d 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 83 deltaM-fmap-equiv {l} {A} {B} {O} {T} {F} {M} {f} {g} eq (deltaM (mono x)) = begin
102 deltaM-is-functor {F = F} = record { fmap = deltaM-fmap 102 deltaM-is-functor {F = F} = record { fmap = deltaM-fmap
103 ; preserve-id = deltaM-preserve-id {F = F} 103 ; preserve-id = deltaM-preserve-id {F = F}
104 ; 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 105 ; fmap-equiv = deltaM-fmap-equiv
106 } 106 }
107
108