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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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 -}