Mercurial > hg > Papers > 2015 > atton-thesis
annotate src/delta_monad_definition.agda @ 57:5f0e13923cfd
Fixes
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 16 Feb 2015 16:24:42 +0900 |
parents | b7e693b6d7d9 |
children |
rev | line source |
---|---|
43
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 open import Level |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 open import Relation.Binary.PropositionalEquality |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 open ≡-Reasoning |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 open import basic |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 open import delta |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 open import delta.functor |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 open import nat |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 open import laws |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 module delta.monad where |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 tailDelta-is-nt : {l : Level} {A B : Set l} {n : Nat} |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 (f : A -> B) -> (d : Delta A (S (S n))) -> |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 (tailDelta {n = n} ∙ (delta-fmap f)) d ≡ ((delta-fmap f) ∙ tailDelta {n = n}) d |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 tailDelta-is-nt f (delta x d) = refl |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 tailDelta-to-tail-nt : {l : Level} {A B : Set l} (n m : Nat) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 (f : A -> B) (d : Delta (Delta A (S (S m))) (S n)) -> |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 delta-fmap tailDelta (delta-fmap (delta-fmap f) d) ≡ delta-fmap (delta-fmap f) (delta-fmap tailDelta d) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 tailDelta-to-tail-nt O O f (mono (delta x d)) = refl |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 tailDelta-to-tail-nt O (S m) f (mono (delta x d)) = refl |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 tailDelta-to-tail-nt (S n) O f (delta (delta x (mono xx)) d) = begin |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 delta (mono (f xx)) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 (delta-fmap tailDelta (delta-fmap (delta-fmap f) d)) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 ≡⟨ cong (\de -> delta (mono (f xx)) de) (tailDelta-to-tail-nt n O f d) ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 delta (mono (f xx)) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 (delta-fmap (delta-fmap f) (delta-fmap tailDelta d)) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 ∎ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 tailDelta-to-tail-nt (S n) (S m) f (delta (delta x (delta xx d)) ds) = begin |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 delta (delta (f xx) (delta-fmap f d)) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 (delta-fmap tailDelta (delta-fmap (delta-fmap f) ds)) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 ≡⟨ cong (\de -> delta (delta (f xx) (delta-fmap f d)) de) (tailDelta-to-tail-nt n (S m) f ds) ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 delta (delta (f xx) (delta-fmap f d)) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
36 (delta-fmap (delta-fmap f) (delta-fmap tailDelta ds)) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
37 ∎ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
38 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
40 delta-eta-is-nt : {l : Level} {A B : Set l} -> {n : Nat} |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 (f : A -> B) -> (x : A) -> (delta-eta {n = n} ∙ f) x ≡ delta-fmap f (delta-eta x) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 delta-eta-is-nt {n = O} f x = refl |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 delta-eta-is-nt {n = S O} f x = refl |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
44 delta-eta-is-nt {n = S n} f x = begin |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 (delta-eta ∙ f) x ≡⟨ refl ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
46 delta-eta (f x) ≡⟨ refl ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
47 delta (f x) (delta-eta (f x)) ≡⟨ cong (\de -> delta (f x) de) (delta-eta-is-nt f x) ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
48 delta (f x) (delta-fmap f (delta-eta x)) ≡⟨ refl ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
49 delta-fmap f (delta x (delta-eta x)) ≡⟨ refl ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
50 delta-fmap f (delta-eta x) ∎ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
51 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
52 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
53 delta-mu-is-nt : {l : Level} {A B : Set l} {n : Nat} -> (f : A -> B) -> (d : Delta (Delta A (S n)) (S n)) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
54 -> delta-mu (delta-fmap (delta-fmap f) d) ≡ delta-fmap f (delta-mu d) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
55 delta-mu-is-nt {n = O} f (mono d) = refl |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
56 delta-mu-is-nt {n = S n} f (delta (delta x d) ds) = begin |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
57 delta (f x) (delta-mu (delta-fmap tailDelta (delta-fmap (delta-fmap f) ds))) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
58 ≡⟨ cong (\de -> delta (f x) (delta-mu de)) (tailDelta-to-tail-nt n n f ds ) ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
59 delta (f x) (delta-mu (delta-fmap (delta-fmap f) (delta-fmap tailDelta ds))) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
60 ≡⟨ cong (\de -> delta (f x) de) (delta-mu-is-nt f (delta-fmap tailDelta ds)) ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
61 delta (f x) (delta-fmap f (delta-mu (delta-fmap tailDelta ds))) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
62 ∎ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
63 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
64 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
65 delta-fmap-mu-to-tail : {l : Level} {A : Set l} (n m : Nat) (d : Delta (Delta (Delta A (S (S m))) (S (S m))) (S n)) -> |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
66 delta-fmap tailDelta (delta-fmap delta-mu d) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
67 ≡ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
68 (delta-fmap delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta d))) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
69 delta-fmap-mu-to-tail O O (mono (delta d ds)) = refl |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
70 delta-fmap-mu-to-tail O (S n) (mono (delta (delta x (delta xx d)) (delta (delta dx (delta dxx dd)) ds))) = refl |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
71 delta-fmap-mu-to-tail (S n) O (delta (delta (delta x (mono xx)) (mono (delta dx (mono dxx)))) ds) = begin |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
72 delta (mono dxx) (delta-fmap tailDelta (delta-fmap delta-mu ds)) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
73 ≡⟨ cong (\de -> delta (mono dxx) de) (delta-fmap-mu-to-tail n O ds) ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
74 delta (mono dxx) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
75 (delta-fmap delta-mu |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
76 (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
77 ∎ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
78 delta-fmap-mu-to-tail (S n) (S n₁) (delta (delta (delta x (delta xx d)) (delta (delta dx (delta dxx dd)) ds)) dds) = begin |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
79 delta (delta dxx (delta-mu (delta-fmap tailDelta (delta-fmap tailDelta ds)))) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
80 (delta-fmap tailDelta (delta-fmap delta-mu dds)) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
81 ≡⟨ cong (\de -> delta (delta dxx (delta-mu (delta-fmap tailDelta (delta-fmap tailDelta ds)))) de) (delta-fmap-mu-to-tail n (S n₁) dds) ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
82 delta (delta dxx (delta-mu (delta-fmap tailDelta (delta-fmap tailDelta ds)))) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
83 (delta-fmap delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta dds))) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
84 ∎ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
85 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
86 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
87 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
88 -- Monad-laws (Category) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
89 -- association-law : join . delta-fmap join = join . join |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
90 delta-association-law : {l : Level} {A : Set l} {n : Nat} (d : Delta (Delta (Delta A (S n)) (S n)) (S n)) -> |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
91 ((delta-mu ∙ (delta-fmap delta-mu)) d) ≡ ((delta-mu ∙ delta-mu) d) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
92 delta-association-law {n = O} (mono d) = refl |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
93 delta-association-law {n = S n} (delta (delta (delta x d) dd) ds) = begin |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
94 delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds))) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
95 ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-fmap-mu-to-tail n n ds) ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
96 delta x (delta-mu (delta-fmap delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds)))) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
97 ≡⟨ cong (\de -> delta x de) (delta-association-law (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))) ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
98 delta x (delta-mu (delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds)))) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
99 ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-mu-is-nt tailDelta (delta-fmap tailDelta ds) ) ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
100 delta x (delta-mu (delta-fmap tailDelta (delta-mu (delta-fmap tailDelta ds)))) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
101 ∎ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
102 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
103 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
104 delta-right-unity-law : {l : Level} {A : Set l} {n : Nat} (d : Delta A (S n)) -> (delta-mu ∙ delta-eta) d ≡ id d |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
105 delta-right-unity-law (mono x) = refl |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
106 delta-right-unity-law (delta x d) = begin |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
107 (delta-mu ∙ delta-eta) (delta x d) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
108 ≡⟨ refl ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
109 delta-mu (delta-eta (delta x d)) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
110 ≡⟨ refl ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
111 delta-mu (delta (delta x d) (delta-eta (delta x d))) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
112 ≡⟨ refl ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
113 delta (headDelta (delta x d)) (delta-mu (delta-fmap tailDelta (delta-eta (delta x d)))) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
114 ≡⟨ refl ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
115 delta x (delta-mu (delta-fmap tailDelta (delta-eta (delta x d)))) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
116 ≡⟨ cong (\de -> delta x (delta-mu de)) (sym (delta-eta-is-nt tailDelta (delta x d))) ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
117 delta x (delta-mu (delta-eta (tailDelta (delta x d)))) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
118 ≡⟨ refl ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
119 delta x (delta-mu (delta-eta d)) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
120 ≡⟨ cong (\de -> delta x de) (delta-right-unity-law d) ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
121 delta x d |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
122 ≡⟨ refl ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
123 id (delta x d) ∎ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
124 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
125 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
126 delta-left-unity-law : {l : Level} {A : Set l} {n : Nat} -> (d : Delta A (S n)) -> |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
127 (delta-mu ∙ (delta-fmap delta-eta)) d ≡ id d |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
128 delta-left-unity-law (mono x) = refl |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
129 delta-left-unity-law {n = (S n)} (delta x d) = begin |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
130 (delta-mu ∙ delta-fmap delta-eta) (delta x d) ≡⟨ refl ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
131 delta-mu ( delta-fmap delta-eta (delta x d)) ≡⟨ refl ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
132 delta-mu (delta (delta-eta x) (delta-fmap delta-eta d)) ≡⟨ refl ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
133 delta (headDelta {n = S n} (delta-eta x)) (delta-mu (delta-fmap tailDelta (delta-fmap delta-eta d))) ≡⟨ refl ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
134 delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-eta d))) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
135 ≡⟨ cong (\de -> delta x (delta-mu de)) (sym (delta-covariant tailDelta delta-eta d)) ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
136 delta x (delta-mu (delta-fmap (tailDelta ∙ delta-eta {n = S n}) d)) ≡⟨ refl ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
137 delta x (delta-mu (delta-fmap (delta-eta {n = n}) d)) ≡⟨ cong (\de -> delta x de) (delta-left-unity-law d) ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
138 delta x d ≡⟨ refl ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
139 id (delta x d) ∎ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
140 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
141 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
142 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
143 delta-is-monad : {l : Level} {n : Nat} -> Monad {l} (\A -> Delta A (S n)) delta-is-functor |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
144 delta-is-monad = record { eta = delta-eta; |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
145 mu = delta-mu; |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
146 eta-is-nt = delta-eta-is-nt; |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
147 mu-is-nt = delta-mu-is-nt; |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
148 association-law = delta-association-law; |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
149 left-unity-law = delta-left-unity-law ; |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
150 right-unity-law = \x -> (sym (delta-right-unity-law x)) } |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
151 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
152 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
153 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
154 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
155 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
156 {- |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
157 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
158 -- Monad-laws (Haskell) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
159 -- monad-law-h-1 : return a >>= k = k a |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
160 monad-law-h-1 : {l : Level} {A B : Set l} -> |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
161 (a : A) -> (k : A -> (Delta B)) -> |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
162 (delta-return a >>= k) ≡ (k a) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
163 monad-law-h-1 a k = refl |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
164 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
165 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
166 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
167 -- monad-law-h-2 : m >>= return = m |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
168 monad-law-h-2 : {l : Level}{A : Set l} -> (m : Delta A) -> (m >>= delta-return) ≡ m |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
169 monad-law-h-2 (mono x) = refl |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
170 monad-law-h-2 (delta x d) = cong (delta x) (monad-law-h-2 d) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
171 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
172 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
173 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
174 -- monad-law-h-3 : m >>= (\x -> f x >>= g) = (m >>= f) >>= g |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
175 monad-law-h-3 : {l : Level} {A B C : Set l} -> |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
176 (m : Delta A) -> (f : A -> (Delta B)) -> (g : B -> (Delta C)) -> |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
177 (delta-bind m (\x -> delta-bind (f x) g)) ≡ (delta-bind (delta-bind m f) g) |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
178 monad-law-h-3 (mono x) f g = refl |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
179 monad-law-h-3 (delta x d) f g = begin |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
180 (delta-bind (delta x d) (\x -> delta-bind (f x) g)) ≡⟨ {!!} ⟩ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
181 (delta-bind (delta-bind (delta x d) f) g) ∎ |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
182 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
183 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
184 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
185 |
b7e693b6d7d9
Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
186 -} |