Mercurial > hg > Members > atton > delta_monad
comparison agda/delta/monad.agda @ 131:d205ff1e406f InfiniteDeltaWithMonad
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 |