Mercurial > hg > Members > atton > delta_monad

comparison agda/delta/monad.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 e1900c89dea9
children b6dcbe8617a9
comparison
equal deleted inserted replaced
130:ac45d065cbf2 131:d205ff1e406f
1 open import Level
2 open import Relation.Binary.PropositionalEquality
3 open ≡-Reasoning
4
1 open import basic 5 open import basic
2 open import delta 6 open import delta
3 open import delta.functor 7 open import delta.functor
4 open import nat 8 open import nat
5 open import laws 9 open import laws
6
7
8 open import Level
9 open import Relation.Binary.PropositionalEquality
10 open ≡-Reasoning
11 10
12 module delta.monad where 11 module delta.monad where
13 12
14 tailDelta-is-nt : {l : Level} {A B : Set l} {n : Nat} 13 tailDelta-is-nt : {l : Level} {A B : Set l} {n : Nat}
15 (f : A -> B) -> (d : Delta A (S (S n))) -> 14 (f : A -> B) -> (d : Delta A (S (S n))) ->
85 ∎ 84 ∎
86 85
87 86
88 87
89 -- Monad-laws (Category) 88 -- Monad-laws (Category)
90 -- monad-law-1 : join . delta-fmap join = join . join 89 -- association-law : join . delta-fmap join = join . join
91 monad-law-1 : {l : Level} {A : Set l} {n : Nat} (d : Delta (Delta (Delta A (S n)) (S n)) (S n)) -> 90 delta-association-law : {l : Level} {A : Set l} {n : Nat} (d : Delta (Delta (Delta A (S n)) (S n)) (S n)) ->
92 ((delta-mu ∙ (delta-fmap delta-mu)) d) ≡ ((delta-mu ∙ delta-mu) d) 91 ((delta-mu ∙ (delta-fmap delta-mu)) d) ≡ ((delta-mu ∙ delta-mu) d)
93 monad-law-1 {n = O} (mono d) = refl 92 delta-association-law {n = O} (mono d) = refl
94 monad-law-1 {n = S n} (delta (delta (delta x d) dd) ds) = begin 93 delta-association-law {n = S n} (delta (delta (delta x d) dd) ds) = begin
95 delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds))) 94 delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds)))
96 ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-fmap-mu-to-tail n n ds) ⟩ 95 ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-fmap-mu-to-tail n n ds) ⟩
97 delta x (delta-mu (delta-fmap delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds)))) 96 delta x (delta-mu (delta-fmap delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))))
98 ≡⟨ cong (\de -> delta x de) (monad-law-1 (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))) ⟩ 97 ≡⟨ cong (\de -> delta x de) (delta-association-law (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))) ⟩
99 delta x (delta-mu (delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds)))) 98 delta x (delta-mu (delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))))
100 ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-mu-is-nt tailDelta (delta-fmap tailDelta ds) ) ⟩ 99 ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-mu-is-nt tailDelta (delta-fmap tailDelta ds) ) ⟩
101 delta x (delta-mu (delta-fmap tailDelta (delta-mu (delta-fmap tailDelta ds)))) 100 delta x (delta-mu (delta-fmap tailDelta (delta-mu (delta-fmap tailDelta ds))))
102 ∎ 101 ∎
103 102
131 (delta-mu ∙ delta-fmap delta-eta) (delta x d) ≡⟨ refl ⟩ 130 (delta-mu ∙ delta-fmap delta-eta) (delta x d) ≡⟨ refl ⟩
132 delta-mu ( delta-fmap delta-eta (delta x d)) ≡⟨ refl ⟩ 131 delta-mu ( delta-fmap delta-eta (delta x d)) ≡⟨ refl ⟩
133 delta-mu (delta (delta-eta x) (delta-fmap delta-eta d)) ≡⟨ refl ⟩ 132 delta-mu (delta (delta-eta x) (delta-fmap delta-eta d)) ≡⟨ refl ⟩
134 delta (headDelta {n = S n} (delta-eta x)) (delta-mu (delta-fmap tailDelta (delta-fmap delta-eta d))) ≡⟨ refl ⟩ 133 delta (headDelta {n = S n} (delta-eta x)) (delta-mu (delta-fmap tailDelta (delta-fmap delta-eta d))) ≡⟨ refl ⟩
135 delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-eta d))) 134 delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-eta d)))
136 ≡⟨ cong (\de -> delta x (delta-mu de)) (sym (functor-law-2 tailDelta delta-eta d)) ⟩ 135 ≡⟨ cong (\de -> delta x (delta-mu de)) (sym (delta-covariant tailDelta delta-eta d)) ⟩
137 delta x (delta-mu (delta-fmap (tailDelta ∙ delta-eta {n = S n}) d)) ≡⟨ refl ⟩ 136 delta x (delta-mu (delta-fmap (tailDelta ∙ delta-eta {n = S n}) d)) ≡⟨ refl ⟩
138 delta x (delta-mu (delta-fmap (delta-eta {n = n}) d)) ≡⟨ cong (\de -> delta x de) (delta-left-unity-law d) ⟩ 137 delta x (delta-mu (delta-fmap (delta-eta {n = n}) d)) ≡⟨ cong (\de -> delta x de) (delta-left-unity-law d) ⟩
139 delta x d ≡⟨ refl ⟩ 138 delta x d ≡⟨ refl ⟩
140 id (delta x d) ∎ 139 id (delta x d) ∎
141 140
144 delta-is-monad : {l : Level} {n : Nat} -> Monad {l} (\A -> Delta A (S n)) delta-is-functor 143 delta-is-monad : {l : Level} {n : Nat} -> Monad {l} (\A -> Delta A (S n)) delta-is-functor
145 delta-is-monad = record { eta = delta-eta; 144 delta-is-monad = record { eta = delta-eta;
146 mu = delta-mu; 145 mu = delta-mu;
147 eta-is-nt = delta-eta-is-nt; 146 eta-is-nt = delta-eta-is-nt;
148 mu-is-nt = delta-mu-is-nt; 147 mu-is-nt = delta-mu-is-nt;
149 association-law = monad-law-1; 148 association-law = delta-association-law;
150 left-unity-law = delta-left-unity-law ; 149 left-unity-law = delta-left-unity-law ;
151 right-unity-law = \x -> (sym (delta-right-unity-law x)) } 150 right-unity-law = \x -> (sym (delta-right-unity-law x)) }
152 151
153 152
154 153