comparison agda/delta/monad.agda @ 105:e6499a50ccbd

Retrying prove monad-laws for delta
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 27 Jan 2015 17:49:25 +0900
parents ebd0d6e2772c
children caaf364f45ac
comparison
equal deleted inserted replaced
104:ebd0d6e2772c 105:e6499a50ccbd
1 open import basic 1 open import basic
2 open import delta 2 open import delta
3 open import delta.functor 3 open import delta.functor
4 open import nat 4 open import nat
5 open import laws 5 open import laws
6 open import revision
7 6
8 7
9 open import Level 8 open import Level
10 open import Relation.Binary.PropositionalEquality 9 open import Relation.Binary.PropositionalEquality
11 open ≡-Reasoning 10 open ≡-Reasoning
12 11
13 module delta.monad where 12 module delta.monad where
14 13
14 delta-eta-is-nt : {l : Level} {A B : Set l} -> {n : Nat}
15 (f : A -> B) -> (x : A) -> (delta-eta {n = n} ∙ f) x ≡ delta-fmap f (delta-eta x)
16 delta-eta-is-nt {n = O} f x = refl
17 delta-eta-is-nt {n = S O} f x = refl
18 delta-eta-is-nt {n = S n} f x = begin
19 (delta-eta ∙ f) x ≡⟨ refl ⟩
20 delta-eta (f x) ≡⟨ refl ⟩
21 delta (f x) (delta-eta (f x)) ≡⟨ cong (\de -> delta (f x) de) (delta-eta-is-nt f x) ⟩
22 delta (f x) (delta-fmap f (delta-eta x)) ≡⟨ refl ⟩
23 delta-fmap f (delta x (delta-eta x)) ≡⟨ refl ⟩
24 delta-fmap f (delta-eta x) ∎
25
26 delta-mu-is-nt : {l : Level} {A B : Set l} {n : Nat} -> (f : A -> B) -> (d : Delta (Delta A (S n)) (S n))
27 -> delta-mu (delta-fmap (delta-fmap f) d) ≡ delta-fmap f (delta-mu d)
28 delta-mu-is-nt f d = {!!}
29
30 hoge : {l : Level} {A : Set l} {n : Nat} -> (ds : Delta (Delta A (S (S n))) (S (S n))) ->
31 (tailDelta {n = n} ∙ delta-mu {n = (S n)}) ds
32
33 (((delta-mu {n = n}) ∙ (delta-fmap tailDelta)) ∙ tailDelta) ds
34 hoge (delta ds ds₁) = refl
35
36
37
15 38
16 -- Monad-laws (Category) 39 -- Monad-laws (Category)
40 -- monad-law-1 : join . delta-fmap join = join . join
41 monad-law-1 : {l : Level} {A : Set l} {n : Nat} (d : Delta (Delta (Delta A (S n)) (S n)) (S n)) ->
42 ((delta-mu ∙ (delta-fmap delta-mu)) d) ≡ ((delta-mu ∙ delta-mu) d)
43 monad-law-1 {n = O} (mono d) = refl
44 monad-law-1 {n = S O} (delta (delta (delta _ _) _) (mono (delta (delta _ (mono _)) (mono (delta _ (mono _)))))) = refl
45 monad-law-1 {n = S n} (delta (delta (delta x d) dd) ds) = begin
46 (delta-mu ∙ delta-fmap delta-mu) (delta (delta (delta x d) dd) ds) ≡⟨ refl ⟩
47 delta-mu (delta-fmap delta-mu (delta (delta (delta x d) dd) ds)) ≡⟨ refl ⟩
48 delta-mu (delta (delta-mu (delta (delta x d) dd)) (delta-fmap delta-mu ds)) ≡⟨ refl ⟩
49 delta-mu (delta (delta (headDelta (delta x d)) (delta-mu (delta-fmap tailDelta dd))) (delta-fmap delta-mu ds)) ≡⟨ refl ⟩
50 delta-mu (delta (delta x (delta-mu (delta-fmap tailDelta dd))) (delta-fmap delta-mu ds)) ≡⟨ refl ⟩
51 delta (headDelta (delta x (delta-mu (delta-fmap tailDelta dd)))) (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds))) ≡⟨ refl ⟩
52 delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds)))
53 ≡⟨ cong (\de -> delta x (delta-mu de)) (sym (functor-law-2 tailDelta delta-mu ds)) ⟩
54 delta x (delta-mu (delta-fmap (tailDelta {n = n} ∙ delta-mu {n = (S n)}) ds))
55 -- ≡⟨ cong (\ff -> delta x (delta-mu (delta-fmap ff ds))) hoge ⟩
56 ≡⟨ {!!} ⟩
57 delta x (delta-mu (delta-fmap (((delta-mu {n = n}) ∙ (delta-fmap tailDelta)) ∙ tailDelta) ds))
58 ≡⟨ cong (\de -> delta x (delta-mu de)) (functor-law-2 (delta-mu ∙ (delta-fmap tailDelta)) tailDelta ds ) ⟩
59 delta x (delta-mu (delta-fmap ((delta-mu {n = n}) ∙ (delta-fmap tailDelta)) (delta-fmap tailDelta ds)))
60 ≡⟨ cong (\de -> delta x (delta-mu de)) (functor-law-2 delta-mu (delta-fmap tailDelta) (delta-fmap tailDelta ds)) ⟩
61 delta x (delta-mu (delta-fmap (delta-mu {n = n}) (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))))
62 ≡⟨ cong (\de -> delta x de) (monad-law-1 (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))) ⟩
63 delta x (delta-mu (delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))))
64 ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-mu-is-nt tailDelta (delta-fmap tailDelta ds)) ⟩
65 delta x (delta-mu (delta-fmap tailDelta (delta-mu (delta-fmap tailDelta ds)))) ≡⟨ refl ⟩
66 delta (headDelta (delta x d)) (delta-mu (delta-fmap tailDelta (delta-mu (delta-fmap tailDelta ds)))) ≡⟨ refl ⟩
67 delta-mu (delta (delta x d) (delta-mu (delta-fmap tailDelta ds))) ≡⟨ refl ⟩
68 delta-mu (delta (headDelta (delta (delta x d) dd)) (delta-mu (delta-fmap tailDelta ds))) ≡⟨ refl ⟩
69 delta-mu (delta-mu (delta (delta (delta x d) dd) ds)) ≡⟨ refl ⟩
70 (delta-mu ∙ delta-mu) (delta (delta (delta x d) dd) ds)
71
17 {- 72 {-
18 73 begin
19 monad-law-1-5 : {l : Level} {A : Set l} -> (m : Nat) (n : Nat) -> (ds : Delta (Delta A)) -> 74 (delta-mu ∙ delta-fmap delta-mu) (delta d ds) ≡⟨ refl ⟩
20 n-tail n (delta-bind ds (n-tail m)) ≡ delta-bind (n-tail n ds) (n-tail (m + n)) 75 delta-mu (delta-fmap delta-mu (delta d ds)) ≡⟨ refl ⟩
21 monad-law-1-5 O O ds = refl 76 delta-mu (delta (delta-mu d) (delta-fmap delta-mu ds)) ≡⟨ refl ⟩
22 monad-law-1-5 O (S n) (mono ds) = begin 77 delta (headDelta (delta-mu d)) (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds))) ≡⟨ {!!} ⟩
23 n-tail (S n) (delta-bind (mono ds) (n-tail O)) ≡⟨ refl ⟩ 78 delta (headDelta (headDelta d)) (delta-mu (delta-fmap tailDelta (delta-mu (delta-fmap tailDelta ds)))) ≡⟨ refl ⟩
24 n-tail (S n) ds ≡⟨ refl ⟩ 79 delta-mu (delta (headDelta d) (delta-mu (delta-fmap tailDelta ds))) ≡⟨ refl ⟩
25 delta-bind (mono ds) (n-tail (S n)) ≡⟨ cong (\de -> delta-bind de (n-tail (S n))) (sym (tail-delta-to-mono (S n) ds)) ⟩ 80 delta-mu (delta-mu (delta d ds)) ≡⟨ refl ⟩
26 delta-bind (n-tail (S n) (mono ds)) (n-tail (S n)) ≡⟨ refl ⟩ 81 (delta-mu ∙ delta-mu) (delta d ds)
27 delta-bind (n-tail (S n) (mono ds)) (n-tail (O + S n))
28 82
29 monad-law-1-5 O (S n) (delta d ds) = begin 83 -}
30 n-tail (S n) (delta-bind (delta d ds) (n-tail O)) ≡⟨ refl ⟩
31 n-tail (S n) (delta (headDelta d) (delta-bind ds tailDelta )) ≡⟨ cong (\t -> t (delta (headDelta d) (delta-bind ds tailDelta ))) (sym (n-tail-plus n)) ⟩
32 ((n-tail n) ∙ tailDelta) (delta (headDelta d) (delta-bind ds tailDelta )) ≡⟨ refl ⟩
33 (n-tail n) (delta-bind ds tailDelta) ≡⟨ monad-law-1-5 (S O) n ds ⟩
34 delta-bind (n-tail n ds) (n-tail (S n)) ≡⟨ refl ⟩
35 delta-bind (((n-tail n) ∙ tailDelta) (delta d ds)) (n-tail (S n)) ≡⟨ cong (\t -> delta-bind (t (delta d ds)) (n-tail (S n))) (n-tail-plus n) ⟩
36 delta-bind (n-tail (S n) (delta d ds)) (n-tail (S n)) ≡⟨ refl ⟩
37 delta-bind (n-tail (S n) (delta d ds)) (n-tail (O + S n))
38
39 monad-law-1-5 (S m) n (mono (mono x)) = begin
40 n-tail n (delta-bind (mono (mono x)) (n-tail (S m))) ≡⟨ refl ⟩
41 n-tail n (n-tail (S m) (mono x)) ≡⟨ cong (\de -> n-tail n de) (tail-delta-to-mono (S m) x)⟩
42 n-tail n (mono x) ≡⟨ tail-delta-to-mono n x ⟩
43 mono x ≡⟨ sym (tail-delta-to-mono (S m + n) x) ⟩
44 (n-tail (S m + n)) (mono x) ≡⟨ refl ⟩
45 delta-bind (mono (mono x)) (n-tail (S m + n)) ≡⟨ cong (\de -> delta-bind de (n-tail (S m + n))) (sym (tail-delta-to-mono n (mono x))) ⟩
46 delta-bind (n-tail n (mono (mono x))) (n-tail (S m + n))
47
48 monad-law-1-5 (S m) n (mono (delta x ds)) = begin
49 n-tail n (delta-bind (mono (delta x ds)) (n-tail (S m))) ≡⟨ refl ⟩
50 n-tail n (n-tail (S m) (delta x ds)) ≡⟨ cong (\t -> n-tail n (t (delta x ds))) (sym (n-tail-plus m)) ⟩
51 n-tail n (((n-tail m) ∙ tailDelta) (delta x ds)) ≡⟨ refl ⟩
52 n-tail n ((n-tail m) ds) ≡⟨ cong (\t -> t ds) (n-tail-add {d = ds} n m) ⟩
53 n-tail (n + m) ds ≡⟨ cong (\n -> n-tail n ds) (nat-add-sym n m) ⟩
54 n-tail (m + n) ds ≡⟨ refl ⟩
55 ((n-tail (m + n)) ∙ tailDelta) (delta x ds) ≡⟨ cong (\t -> t (delta x ds)) (n-tail-plus (m + n))⟩
56 n-tail (S (m + n)) (delta x ds) ≡⟨ refl ⟩
57 n-tail (S m + n) (delta x ds) ≡⟨ refl ⟩
58 delta-bind (mono (delta x ds)) (n-tail (S m + n)) ≡⟨ cong (\de -> delta-bind de (n-tail (S m + n))) (sym (tail-delta-to-mono n (delta x ds))) ⟩
59 delta-bind (n-tail n (mono (delta x ds))) (n-tail (S m + n))
60
61 monad-law-1-5 (S m) O (delta d ds) = begin
62 n-tail O (delta-bind (delta d ds) (n-tail (S m))) ≡⟨ refl ⟩
63 (delta-bind (delta d ds) (n-tail (S m))) ≡⟨ refl ⟩
64 delta (headDelta ((n-tail (S m)) d)) (delta-bind ds (tailDelta ∙ (n-tail (S m)))) ≡⟨ refl ⟩
65 delta-bind (delta d ds) (n-tail (S m)) ≡⟨ refl ⟩
66 delta-bind (n-tail O (delta d ds)) (n-tail (S m)) ≡⟨ cong (\n -> delta-bind (n-tail O (delta d ds)) (n-tail n)) (nat-add-right-zero (S m)) ⟩
67 delta-bind (n-tail O (delta d ds)) (n-tail (S m + O))
68
69 monad-law-1-5 (S m) (S n) (delta d ds) = begin
70 n-tail (S n) (delta-bind (delta d ds) (n-tail (S m))) ≡⟨ cong (\t -> t ((delta-bind (delta d ds) (n-tail (S m))))) (sym (n-tail-plus n)) ⟩
71 ((n-tail n) ∙ tailDelta) (delta-bind (delta d ds) (n-tail (S m))) ≡⟨ refl ⟩
72 ((n-tail n) ∙ tailDelta) (delta (headDelta ((n-tail (S m)) d)) (delta-bind ds (tailDelta ∙ (n-tail (S m))))) ≡⟨ refl ⟩
73 (n-tail n) (delta-bind ds (tailDelta ∙ (n-tail (S m)))) ≡⟨ refl ⟩
74 (n-tail n) (delta-bind ds (n-tail (S (S m)))) ≡⟨ monad-law-1-5 (S (S m)) n ds ⟩
75 delta-bind ((n-tail n) ds) (n-tail (S (S (m + n)))) ≡⟨ cong (\nm -> delta-bind ((n-tail n) ds) (n-tail nm)) (sym (nat-right-increment (S m) n)) ⟩
76 delta-bind ((n-tail n) ds) (n-tail (S m + S n)) ≡⟨ refl ⟩
77 delta-bind (((n-tail n) ∙ tailDelta) (delta d ds)) (n-tail (S m + S n)) ≡⟨ cong (\t -> delta-bind (t (delta d ds)) (n-tail (S m + S n))) (n-tail-plus n) ⟩
78 delta-bind (n-tail (S n) (delta d ds)) (n-tail (S m + S n))
79
80
81 monad-law-1-4 : {l : Level} {A : Set l} -> (m n : Nat) -> (dd : Delta (Delta A)) ->
82 headDelta ((n-tail n) (delta-bind dd (n-tail m))) ≡ headDelta ((n-tail (m + n)) (headDelta (n-tail n dd)))
83 monad-law-1-4 O O (mono dd) = refl
84 monad-law-1-4 O O (delta dd dd₁) = refl
85 monad-law-1-4 O (S n) (mono dd) = begin
86 headDelta (n-tail (S n) (delta-bind (mono dd) (n-tail O))) ≡⟨ refl ⟩
87 headDelta (n-tail (S n) dd) ≡⟨ refl ⟩
88 headDelta (n-tail (S n) (headDelta (mono dd))) ≡⟨ cong (\de -> headDelta (n-tail (S n) (headDelta de))) (sym (tail-delta-to-mono (S n) dd)) ⟩
89 headDelta (n-tail (S n) (headDelta (n-tail (S n) (mono dd)))) ≡⟨ refl ⟩
90 headDelta (n-tail (O + S n) (headDelta (n-tail (S n) (mono dd))))
91
92 monad-law-1-4 O (S n) (delta d ds) = begin
93 headDelta (n-tail (S n) (delta-bind (delta d ds) (n-tail O))) ≡⟨ refl ⟩
94 headDelta (n-tail (S n) (delta-bind (delta d ds) id)) ≡⟨ refl ⟩
95 headDelta (n-tail (S n) (delta (headDelta d) (delta-bind ds tailDelta))) ≡⟨ cong (\t -> headDelta (t (delta (headDelta d) (delta-bind ds tailDelta)))) (sym (n-tail-plus n)) ⟩
96 headDelta (((n-tail n) ∙ tailDelta) (delta (headDelta d) (delta-bind ds tailDelta))) ≡⟨ refl ⟩
97 headDelta (n-tail n (delta-bind ds tailDelta)) ≡⟨ monad-law-1-4 (S O) n ds ⟩
98 headDelta (n-tail (S n) (headDelta (n-tail n ds))) ≡⟨ refl ⟩
99 headDelta (n-tail (S n) (headDelta (((n-tail n) ∙ tailDelta) (delta d ds)))) ≡⟨ cong (\t -> headDelta (n-tail (S n) (headDelta (t (delta d ds))))) (n-tail-plus n) ⟩
100 headDelta (n-tail (S n) (headDelta (n-tail (S n) (delta d ds)))) ≡⟨ refl ⟩
101 headDelta (n-tail (O + S n) (headDelta (n-tail (S n) (delta d ds))))
102
103 monad-law-1-4 (S m) n (mono dd) = begin
104 headDelta (n-tail n (delta-bind (mono dd) (n-tail (S m)))) ≡⟨ refl ⟩
105 headDelta (n-tail n ((n-tail (S m)) dd)) ≡⟨ cong (\t -> headDelta (t dd)) (n-tail-add {d = dd} n (S m)) ⟩
106 headDelta (n-tail (n + S m) dd) ≡⟨ cong (\n -> headDelta ((n-tail n) dd)) (nat-add-sym n (S m)) ⟩
107 headDelta (n-tail (S m + n) dd) ≡⟨ refl ⟩
108 headDelta (n-tail (S m + n) (headDelta (mono dd))) ≡⟨ cong (\de -> headDelta (n-tail (S m + n) (headDelta de))) (sym (tail-delta-to-mono n dd)) ⟩
109 headDelta (n-tail (S m + n) (headDelta (n-tail n (mono dd))))
110
111 monad-law-1-4 (S m) O (delta d ds) = begin
112 headDelta (n-tail O (delta-bind (delta d ds) (n-tail (S m)))) ≡⟨ refl ⟩
113 headDelta (delta-bind (delta d ds) (n-tail (S m))) ≡⟨ refl ⟩
114 headDelta (delta (headDelta ((n-tail (S m) d))) (delta-bind ds (tailDelta ∙ (n-tail (S m))))) ≡⟨ refl ⟩
115 headDelta (n-tail (S m) d) ≡⟨ cong (\n -> headDelta ((n-tail n) d)) (nat-add-right-zero (S m)) ⟩
116 headDelta (n-tail (S m + O) d) ≡⟨ refl ⟩
117 headDelta (n-tail (S m + O) (headDelta (delta d ds))) ≡⟨ refl ⟩
118 headDelta (n-tail (S m + O) (headDelta (n-tail O (delta d ds))))
119
120 monad-law-1-4 (S m) (S n) (delta d ds) = begin
121 headDelta (n-tail (S n) (delta-bind (delta d ds) (n-tail (S m)))) ≡⟨ refl ⟩
122 headDelta (n-tail (S n) (delta (headDelta ((n-tail (S m)) d)) (delta-bind ds (tailDelta ∙ (n-tail (S m)))))) ≡⟨ cong (\t -> headDelta (t (delta (headDelta ((n-tail (S m)) d)) (delta-bind ds (tailDelta ∙ (n-tail (S m))))))) (sym (n-tail-plus n)) ⟩
123 headDelta ((((n-tail n) ∙ tailDelta) (delta (headDelta ((n-tail (S m)) d)) (delta-bind ds (tailDelta ∙ (n-tail (S m))))))) ≡⟨ refl ⟩
124 headDelta (n-tail n (delta-bind ds (tailDelta ∙ (n-tail (S m))))) ≡⟨ refl ⟩
125 headDelta (n-tail n (delta-bind ds (n-tail (S (S m))))) ≡⟨ monad-law-1-4 (S (S m)) n ds ⟩
126 headDelta (n-tail ((S (S m) + n)) (headDelta (n-tail n ds))) ≡⟨ cong (\nm -> headDelta ((n-tail nm) (headDelta (n-tail n ds)))) (sym (nat-right-increment (S m) n)) ⟩
127 headDelta (n-tail (S m + S n) (headDelta (n-tail n ds))) ≡⟨ refl ⟩
128 headDelta (n-tail (S m + S n) (headDelta (((n-tail n) ∙ tailDelta) (delta d ds)))) ≡⟨ cong (\t -> headDelta (n-tail (S m + S n) (headDelta (t (delta d ds))))) (n-tail-plus n) ⟩
129 headDelta (n-tail (S m + S n) (headDelta (n-tail (S n) (delta d ds))))
130
131
132 monad-law-1-2 : {l : Level} {A : Set l} -> (d : Delta (Delta A)) -> headDelta (delta-mu d) ≡ (headDelta (headDelta d))
133 monad-law-1-2 (mono _) = refl
134 monad-law-1-2 (delta _ _) = refl
135
136 monad-law-1-3 : {l : Level} {A : Set l} -> (n : Nat) -> (d : Delta (Delta (Delta A))) ->
137 delta-bind (delta-fmap delta-mu d) (n-tail n) ≡ delta-bind (delta-bind d (n-tail n)) (n-tail n)
138 monad-law-1-3 O (mono d) = refl
139 monad-law-1-3 O (delta d ds) = begin
140 delta-bind (delta-fmap delta-mu (delta d ds)) (n-tail O) ≡⟨ refl ⟩
141 delta-bind (delta (delta-mu d) (delta-fmap delta-mu ds)) (n-tail O) ≡⟨ refl ⟩
142 delta (headDelta (delta-mu d)) (delta-bind (delta-fmap delta-mu ds) tailDelta) ≡⟨ cong (\dx -> delta dx (delta-bind (delta-fmap delta-mu ds) tailDelta)) (monad-law-1-2 d) ⟩
143 delta (headDelta (headDelta d)) (delta-bind (delta-fmap delta-mu ds) tailDelta) ≡⟨ cong (\dx -> delta (headDelta (headDelta d)) dx) (monad-law-1-3 (S O) ds) ⟩
144 delta (headDelta (headDelta d)) (delta-bind (delta-bind ds tailDelta) tailDelta) ≡⟨ refl ⟩
145 delta-bind (delta (headDelta d) (delta-bind ds tailDelta)) (n-tail O) ≡⟨ refl ⟩
146 delta-bind (delta-bind (delta d ds) (n-tail O)) (n-tail O)
147
148 monad-law-1-3 (S n) (mono (mono d)) = begin
149 delta-bind (delta-fmap delta-mu (mono (mono d))) (n-tail (S n)) ≡⟨ refl ⟩
150 delta-bind (mono d) (n-tail (S n)) ≡⟨ refl ⟩
151 (n-tail (S n)) d ≡⟨ refl ⟩
152 delta-bind (mono d) (n-tail (S n)) ≡⟨ cong (\t -> delta-bind t (n-tail (S n))) (sym (tail-delta-to-mono (S n) d))⟩
153 delta-bind (n-tail (S n) (mono d)) (n-tail (S n)) ≡⟨ refl ⟩
154 delta-bind (n-tail (S n) (mono d)) (n-tail (S n)) ≡⟨ refl ⟩
155 delta-bind (delta-bind (mono (mono d)) (n-tail (S n))) (n-tail (S n))
156
157 monad-law-1-3 (S n) (mono (delta d ds)) = begin
158 delta-bind (delta-fmap delta-mu (mono (delta d ds))) (n-tail (S n)) ≡⟨ refl ⟩
159 delta-bind (mono (delta-mu (delta d ds))) (n-tail (S n)) ≡⟨ refl ⟩
160 n-tail (S n) (delta-mu (delta d ds)) ≡⟨ refl ⟩
161 n-tail (S n) (delta (headDelta d) (delta-bind ds tailDelta)) ≡⟨ cong (\t -> t (delta (headDelta d) (delta-bind ds tailDelta))) (sym (n-tail-plus n)) ⟩
162 (n-tail n ∙ tailDelta) (delta (headDelta d) (delta-bind ds tailDelta)) ≡⟨ refl ⟩
163 n-tail n (delta-bind ds tailDelta) ≡⟨ monad-law-1-5 (S O) n ds ⟩
164 delta-bind (n-tail n ds) (n-tail (S n)) ≡⟨ refl ⟩
165 delta-bind (((n-tail n) ∙ tailDelta) (delta d ds)) (n-tail (S n)) ≡⟨ cong (\t -> (delta-bind (t (delta d ds)) (n-tail (S n)))) (n-tail-plus n) ⟩
166 delta-bind (n-tail (S n) (delta d ds)) (n-tail (S n)) ≡⟨ refl ⟩
167 delta-bind (delta-bind (mono (delta d ds)) (n-tail (S n))) (n-tail (S n))
168
169 monad-law-1-3 (S n) (delta (mono d) ds) = begin
170 delta-bind (delta-fmap delta-mu (delta (mono d) ds)) (n-tail (S n)) ≡⟨ refl ⟩
171 delta-bind (delta (delta-mu (mono d)) (delta-fmap delta-mu ds)) (n-tail (S n)) ≡⟨ refl ⟩
172 delta-bind (delta d (delta-fmap delta-mu ds)) (n-tail (S n)) ≡⟨ refl ⟩
173 delta (headDelta ((n-tail (S n)) d)) (delta-bind (delta-fmap delta-mu ds) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩
174 delta (headDelta ((n-tail (S n)) d)) (delta-bind (delta-fmap delta-mu ds) (n-tail (S (S n)))) ≡⟨ cong (\de -> delta (headDelta ((n-tail (S n)) d)) de) (monad-law-1-3 (S (S n)) ds) ⟩
175 delta (headDelta ((n-tail (S n)) d)) (delta-bind (delta-bind ds (n-tail (S (S n)))) (n-tail (S (S n)))) ≡⟨ refl ⟩
176 delta (headDelta ((n-tail (S n)) d)) (delta-bind (delta-bind ds (tailDelta ∙ (n-tail (S n)))) (n-tail (S (S n)))) ≡⟨ refl ⟩
177 delta (headDelta ((n-tail (S n)) d)) (delta-bind (delta-bind ds (tailDelta ∙ (n-tail (S n)))) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩
178 delta (headDelta ((n-tail (S n)) (headDelta (mono d)))) (delta-bind (delta-bind ds (tailDelta ∙ (n-tail (S n)))) (tailDelta ∙ (n-tail (S n)))) ≡⟨ cong (\de -> delta (headDelta ((n-tail (S n)) (headDelta de))) (delta-bind (delta-bind ds (tailDelta ∙ (n-tail (S n)))) (tailDelta ∙ (n-tail (S n))))) (sym (tail-delta-to-mono (S n) d)) ⟩
179 delta (headDelta ((n-tail (S n)) (headDelta ((n-tail (S n)) (mono d))))) (delta-bind (delta-bind ds (tailDelta ∙ (n-tail (S n)))) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩
180 delta-bind (delta (headDelta ((n-tail (S n)) (mono d))) (delta-bind ds (tailDelta ∙ (n-tail (S n))))) (n-tail (S n)) ≡⟨ refl ⟩
181 delta-bind (delta-bind (delta (mono d) ds) (n-tail (S n))) (n-tail (S n))
182
183 monad-law-1-3 (S n) (delta (delta d dd) ds) = begin
184 delta-bind (delta-fmap delta-mu (delta (delta d dd) ds)) (n-tail (S n)) ≡⟨ refl ⟩
185 delta-bind (delta (delta-mu (delta d dd)) (delta-fmap delta-mu ds)) (n-tail (S n)) ≡⟨ refl ⟩
186 delta (headDelta ((n-tail (S n)) (delta-mu (delta d dd)))) (delta-bind (delta-fmap delta-mu ds) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩
187 delta (headDelta ((n-tail (S n)) (delta (headDelta d) (delta-bind dd tailDelta)))) (delta-bind (delta-fmap delta-mu ds) (tailDelta ∙ (n-tail (S n)))) ≡⟨ cong (\t -> delta (headDelta (t (delta (headDelta d) (delta-bind dd tailDelta)))) (delta-bind (delta-fmap delta-mu ds) (tailDelta ∙ (n-tail (S n)))))(sym (n-tail-plus n)) ⟩
188 delta (headDelta (((n-tail n) ∙ tailDelta) (delta (headDelta d) (delta-bind dd tailDelta)))) (delta-bind (delta-fmap delta-mu ds) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩
189 delta (headDelta ((n-tail n) (delta-bind dd tailDelta))) (delta-bind (delta-fmap delta-mu ds) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩
190 delta (headDelta ((n-tail n) (delta-bind dd tailDelta))) (delta-bind (delta-fmap delta-mu ds) (n-tail (S (S n)))) ≡⟨ cong (\de -> delta (headDelta ((n-tail n) (delta-bind dd tailDelta))) de) (monad-law-1-3 (S (S n)) ds) ⟩
191 delta (headDelta ((n-tail n) (delta-bind dd tailDelta))) (delta-bind (delta-bind ds (n-tail (S (S n)))) (n-tail (S (S n)))) ≡⟨ cong (\de -> delta de ( (delta-bind (delta-bind ds (n-tail (S (S n)))) (n-tail (S (S n)))))) (monad-law-1-4 (S O) n dd) ⟩
192 delta (headDelta ((n-tail (S n)) (headDelta (n-tail n dd)))) (delta-bind (delta-bind ds (n-tail (S (S n)))) (n-tail (S (S n)))) ≡⟨ refl ⟩
193 delta (headDelta ((n-tail (S n)) (headDelta (n-tail n dd)))) (delta-bind (delta-bind ds (n-tail (S (S n)))) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩
194 delta (headDelta ((n-tail (S n)) (headDelta (n-tail n dd)))) (delta-bind (delta-bind ds (tailDelta ∙ (n-tail (S n)))) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩
195 delta (headDelta ((n-tail (S n)) (headDelta (((n-tail n) ∙ tailDelta) (delta d dd))))) (delta-bind (delta-bind ds (tailDelta ∙ (n-tail (S n)))) (tailDelta ∙ (n-tail (S n)))) ≡⟨ cong (\t -> delta (headDelta ((n-tail (S n)) (headDelta (t (delta d dd))))) (delta-bind (delta-bind ds (tailDelta ∙ (n-tail (S n)))) (tailDelta ∙ (n-tail (S n))))) (n-tail-plus n) ⟩
196 delta (headDelta ((n-tail (S n)) (headDelta ((n-tail (S n)) (delta d dd))))) (delta-bind (delta-bind ds (tailDelta ∙ (n-tail (S n)))) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩
197 delta-bind (delta (headDelta ((n-tail (S n)) (delta d dd))) (delta-bind ds (tailDelta ∙ (n-tail (S n))))) (n-tail (S n)) ≡⟨ refl ⟩
198 delta-bind (delta-bind (delta (delta d dd) ds) (n-tail (S n))) (n-tail (S n))
199
200 84
201 85
202 -- monad-law-1 : join . delta-fmap join = join . join
203 monad-law-1 : {l : Level} {A : Set l} -> (d : Delta (Delta (Delta A))) -> ((delta-mu ∙ (delta-fmap delta-mu)) d) ≡ ((delta-mu ∙ delta-mu) d)
204 monad-law-1 (mono d) = refl
205 monad-law-1 (delta x d) = begin
206 (delta-mu ∙ delta-fmap delta-mu) (delta x d) ≡⟨ refl ⟩
207 delta-mu (delta-fmap delta-mu (delta x d)) ≡⟨ refl ⟩
208 delta-mu (delta (delta-mu x) (delta-fmap delta-mu d)) ≡⟨ refl ⟩
209 delta (headDelta (delta-mu x)) (delta-bind (delta-fmap delta-mu d) tailDelta) ≡⟨ cong (\x -> delta x (delta-bind (delta-fmap delta-mu d) tailDelta)) (monad-law-1-2 x) ⟩
210 delta (headDelta (headDelta x)) (delta-bind (delta-fmap delta-mu d) tailDelta) ≡⟨ cong (\d -> delta (headDelta (headDelta x)) d) (monad-law-1-3 (S O) d) ⟩
211 delta (headDelta (headDelta x)) (delta-bind (delta-bind d tailDelta) tailDelta) ≡⟨ refl ⟩
212 delta-mu (delta (headDelta x) (delta-bind d tailDelta)) ≡⟨ refl ⟩
213 delta-mu (delta-mu (delta x d)) ≡⟨ refl ⟩
214 (delta-mu ∙ delta-mu) (delta x d)
215
216 86
217 87
218 monad-law-2-1 : {l : Level} {A : Set l} -> (n : Nat) -> (d : Delta A) -> (delta-bind (delta-fmap delta-eta d) (n-tail n)) ≡ d 88 delta-right-unity-law : {l : Level} {A : Set l} {n : Nat} (d : Delta A (S n)) -> (delta-mu ∙ delta-eta) d ≡ id d
219 monad-law-2-1 O (mono x) = refl 89 delta-right-unity-law (mono x) = refl
220 monad-law-2-1 O (delta x d) = begin 90 delta-right-unity-law (delta x d) = begin
221 delta-bind (delta-fmap delta-eta (delta x d)) (n-tail O) ≡⟨ refl ⟩ 91 (delta-mu ∙ delta-eta) (delta x d)
222 delta-bind (delta (delta-eta x) (delta-fmap delta-eta d)) id ≡⟨ refl ⟩ 92 ≡⟨ refl ⟩
223 delta (headDelta (delta-eta x)) (delta-bind (delta-fmap delta-eta d) tailDelta) ≡⟨ refl ⟩ 93 delta-mu (delta-eta (delta x d))
224 delta x (delta-bind (delta-fmap delta-eta d) tailDelta) ≡⟨ cong (\de -> delta x de) (monad-law-2-1 (S O) d) ⟩ 94 ≡⟨ refl ⟩
225 delta x d ∎ 95 delta-mu (delta (delta x d) (delta-eta (delta x d)))
226 monad-law-2-1 (S n) (mono x) = begin 96 ≡⟨ refl ⟩
227 delta-bind (delta-fmap delta-eta (mono x)) (n-tail (S n)) ≡⟨ refl ⟩ 97 delta (headDelta (delta x d)) (delta-mu (delta-fmap tailDelta (delta-eta (delta x d))))
228 delta-bind (mono (mono x)) (n-tail (S n)) ≡⟨ refl ⟩ 98 ≡⟨ refl ⟩
229 n-tail (S n) (mono x) ≡⟨ tail-delta-to-mono (S n) x ⟩ 99 delta x (delta-mu (delta-fmap tailDelta (delta-eta (delta x d))))
230 mono x ∎ 100 ≡⟨ cong (\de -> delta x (delta-mu de)) (sym (delta-eta-is-nt tailDelta (delta x d))) ⟩
231 monad-law-2-1 (S n) (delta x d) = begin 101 delta x (delta-mu (delta-eta (tailDelta (delta x d))))
232 delta-bind (delta-fmap delta-eta (delta x d)) (n-tail (S n)) ≡⟨ refl ⟩ 102 ≡⟨ refl ⟩
233 delta-bind (delta (delta-eta x) (delta-fmap delta-eta d)) (n-tail (S n)) ≡⟨ refl ⟩ 103 delta x (delta-mu (delta-eta d))
234 delta (headDelta ((n-tail (S n) (delta-eta x)))) (delta-bind (delta-fmap delta-eta d) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩ 104 ≡⟨ cong (\de -> delta x de) (delta-right-unity-law d) ⟩
235 delta (headDelta ((n-tail (S n) (delta-eta x)))) (delta-bind (delta-fmap delta-eta d) (n-tail (S (S n)))) ≡⟨ cong (\de -> delta (headDelta (de)) (delta-bind (delta-fmap delta-eta d) (n-tail (S (S n))))) (tail-delta-to-mono (S n) x) ⟩
236 delta (headDelta (delta-eta x)) (delta-bind (delta-fmap delta-eta d) (n-tail (S (S n)))) ≡⟨ refl ⟩
237 delta x (delta-bind (delta-fmap delta-eta d) (n-tail (S (S n)))) ≡⟨ cong (\d -> delta x d) (monad-law-2-1 (S (S n)) d) ⟩
238 delta x d 105 delta x d
239 106 ≡⟨ refl ⟩
107 id (delta x d) ∎
240 108
241 109
242 -- monad-law-2 : join . delta-fmap return = join . return = id 110 delta-left-unity-law : {l : Level} {A : Set l} {n : Nat} -> (d : Delta A (S n)) ->
243 -- monad-law-2 join . delta-fmap return = join . return 111 (delta-mu ∙ (delta-fmap delta-eta)) d ≡ id d
244 monad-law-2 : {l : Level} {A : Set l} -> (d : Delta A) -> 112 delta-left-unity-law (mono x) = refl
245 (delta-mu ∙ delta-fmap delta-eta) d ≡ (delta-mu ∙ delta-eta) d 113 delta-left-unity-law {n = (S n)} (delta x d) = begin
246 monad-law-2 (mono x) = refl 114 (delta-mu ∙ delta-fmap delta-eta) (delta x d) ≡⟨ refl ⟩
247 monad-law-2 (delta x d) = begin 115 delta-mu ( delta-fmap delta-eta (delta x d)) ≡⟨ refl ⟩
248 (delta-mu ∙ delta-fmap delta-eta) (delta x d) ≡⟨ refl ⟩ 116 delta-mu (delta (delta-eta x) (delta-fmap delta-eta d)) ≡⟨ refl ⟩
249 delta-mu (delta-fmap delta-eta (delta x d)) ≡⟨ refl ⟩ 117 delta (headDelta {n = S n} (delta-eta x)) (delta-mu (delta-fmap tailDelta (delta-fmap delta-eta d))) ≡⟨ refl ⟩
250 delta-mu (delta (mono x) (delta-fmap delta-eta d)) ≡⟨ refl ⟩ 118 delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-eta d)))
251 delta (headDelta (mono x)) (delta-bind (delta-fmap delta-eta d) tailDelta) ≡⟨ refl ⟩ 119 ≡⟨ cong (\de -> delta x (delta-mu de)) (sym (functor-law-2 tailDelta delta-eta d)) ⟩
252 delta x (delta-bind (delta-fmap delta-eta d) tailDelta) ≡⟨ cong (\d -> delta x d) (monad-law-2-1 (S O) d) ⟩ 120 delta x (delta-mu (delta-fmap (tailDelta ∙ delta-eta {n = S n}) d)) ≡⟨ refl ⟩
253 (delta x d) ≡⟨ refl ⟩ 121 delta x (delta-mu (delta-fmap (delta-eta {n = n}) d)) ≡⟨ cong (\de -> delta x de) (delta-left-unity-law d) ⟩
254 delta-mu (mono (delta x d)) ≡⟨ refl ⟩ 122 delta x d ≡⟨ refl ⟩
255 delta-mu (delta-eta (delta x d)) ≡⟨ refl ⟩ 123 id (delta x d) ∎
256 (delta-mu ∙ delta-eta) (delta x d)
257
258 124
259 125
260 -- monad-law-2' : join . return = id
261 monad-law-2' : {l : Level} {A : Set l} -> (d : Delta A) -> (delta-mu ∙ delta-eta) d ≡ id d
262 monad-law-2' d = refl
263 126
264 127 delta-is-monad : {l : Level} {n : Nat} -> Monad {l} (\A -> Delta A (S n)) delta-is-functor
265 -- monad-law-3 : return . f = delta-fmap f . return
266 monad-law-3 : {l : Level} {A B : Set l} (f : A -> B) (x : A) -> (delta-eta ∙ f) x ≡ (delta-fmap f ∙ delta-eta) x
267 monad-law-3 f x = refl
268
269
270 monad-law-4-1 : {l : Level} {A B : Set l} -> (n : Nat) -> (f : A -> B) -> (ds : Delta (Delta A)) ->
271 delta-bind (delta-fmap (delta-fmap f) ds) (n-tail n) ≡ delta-fmap f (delta-bind ds (n-tail n))
272 monad-law-4-1 O f (mono d) = refl
273 monad-law-4-1 O f (delta d ds) = begin
274 delta-bind (delta-fmap (delta-fmap f) (delta d ds)) (n-tail O) ≡⟨ refl ⟩
275 delta-bind (delta (delta-fmap f d) (delta-fmap (delta-fmap f) ds)) (n-tail O) ≡⟨ refl ⟩
276 delta (headDelta (delta-fmap f d)) (delta-bind (delta-fmap (delta-fmap f) ds) tailDelta) ≡⟨ cong (\de -> delta de (delta-bind (delta-fmap (delta-fmap f) ds) tailDelta)) (head-delta-natural-transformation f d) ⟩
277 delta (f (headDelta d)) (delta-bind (delta-fmap (delta-fmap f) ds) tailDelta) ≡⟨ cong (\de -> delta (f (headDelta d)) de) (monad-law-4-1 (S O) f ds) ⟩
278 delta (f (headDelta d)) (delta-fmap f (delta-bind ds tailDelta)) ≡⟨ refl ⟩
279 delta-fmap f (delta (headDelta d) (delta-bind ds tailDelta)) ≡⟨ refl ⟩
280 delta-fmap f (delta-bind (delta d ds) (n-tail O)) ∎
281 monad-law-4-1 (S n) f (mono d) = begin
282 delta-bind (delta-fmap (delta-fmap f) (mono d)) (n-tail (S n)) ≡⟨ refl ⟩
283 delta-bind (mono (delta-fmap f d)) (n-tail (S n)) ≡⟨ refl ⟩
284 n-tail (S n) (delta-fmap f d) ≡⟨ n-tail-natural-transformation (S n) f d ⟩
285 delta-fmap f (n-tail (S n) d) ≡⟨ refl ⟩
286 delta-fmap f (delta-bind (mono d) (n-tail (S n)))
287
288 monad-law-4-1 (S n) f (delta d ds) = begin
289 delta-bind (delta-fmap (delta-fmap f) (delta d ds)) (n-tail (S n)) ≡⟨ refl ⟩
290 delta (headDelta (n-tail (S n) (delta-fmap f d))) (delta-bind (delta-fmap (delta-fmap f) ds) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩
291 delta (headDelta (n-tail (S n) (delta-fmap f d))) (delta-bind (delta-fmap (delta-fmap f) ds) (n-tail (S (S n)))) ≡⟨ cong (\de -> delta (headDelta de) (delta-bind (delta-fmap (delta-fmap f) ds) (n-tail (S (S n))))) (n-tail-natural-transformation (S n) f d) ⟩
292 delta (headDelta (delta-fmap f ((n-tail (S n) d)))) (delta-bind (delta-fmap (delta-fmap f) ds) (n-tail (S (S n)))) ≡⟨ cong (\de -> delta de (delta-bind (delta-fmap (delta-fmap f) ds) (n-tail (S (S n))))) (head-delta-natural-transformation f (n-tail (S n) d)) ⟩
293 delta (f (headDelta (n-tail (S n) d))) (delta-bind (delta-fmap (delta-fmap f) ds) (n-tail (S (S n)))) ≡⟨ cong (\de -> delta (f (headDelta (n-tail (S n) d))) de) (monad-law-4-1 (S (S n)) f ds) ⟩
294 delta (f (headDelta (n-tail (S n) d))) (delta-fmap f (delta-bind ds (n-tail (S (S n))))) ≡⟨ refl ⟩
295 delta-fmap f (delta (headDelta (n-tail (S n) d)) (delta-bind ds (n-tail (S (S n))))) ≡⟨ refl ⟩
296 delta-fmap f (delta (headDelta (n-tail (S n) d)) (delta-bind ds (tailDelta ∙ (n-tail (S n))))) ≡⟨ refl ⟩
297 delta-fmap f (delta-bind (delta d ds) (n-tail (S n))) ∎
298
299
300 -- monad-law-4 : join . delta-fmap (delta-fmap f) = delta-fmap f . join
301 monad-law-4 : {l : Level} {A B : Set l} (f : A -> B) (d : Delta (Delta A)) ->
302 (delta-mu ∙ delta-fmap (delta-fmap f)) d ≡ (delta-fmap f ∙ delta-mu) d
303 monad-law-4 f (mono d) = refl
304 monad-law-4 f (delta (mono x) ds) = begin
305 (delta-mu ∙ delta-fmap (delta-fmap f)) (delta (mono x) ds) ≡⟨ refl ⟩
306 delta-mu ( delta-fmap (delta-fmap f) (delta (mono x) ds)) ≡⟨ refl ⟩
307 delta-mu (delta (mono (f x)) (delta-fmap (delta-fmap f) ds)) ≡⟨ refl ⟩
308 delta (headDelta (mono (f x))) (delta-bind (delta-fmap (delta-fmap f) ds) tailDelta) ≡⟨ refl ⟩
309 delta (f x) (delta-bind (delta-fmap (delta-fmap f) ds) tailDelta) ≡⟨ cong (\de -> delta (f x) de) (monad-law-4-1 (S O) f ds) ⟩
310 delta (f x) (delta-fmap f (delta-bind ds tailDelta)) ≡⟨ refl ⟩
311 delta-fmap f (delta x (delta-bind ds tailDelta)) ≡⟨ refl ⟩
312 delta-fmap f (delta (headDelta (mono x)) (delta-bind ds tailDelta)) ≡⟨ refl ⟩
313 delta-fmap f (delta-mu (delta (mono x) ds)) ≡⟨ refl ⟩
314 (delta-fmap f ∙ delta-mu) (delta (mono x) ds) ∎
315 monad-law-4 f (delta (delta x d) ds) = begin
316 (delta-mu ∙ delta-fmap (delta-fmap f)) (delta (delta x d) ds) ≡⟨ refl ⟩
317 delta-mu (delta-fmap (delta-fmap f) (delta (delta x d) ds)) ≡⟨ refl ⟩
318 delta-mu (delta (delta (f x) (delta-fmap f d)) (delta-fmap (delta-fmap f) ds)) ≡⟨ refl ⟩
319 delta (headDelta (delta (f x) (delta-fmap f d))) (delta-bind (delta-fmap (delta-fmap f) ds) tailDelta) ≡⟨ refl ⟩
320 delta (f x) (delta-bind (delta-fmap (delta-fmap f) ds) tailDelta) ≡⟨ cong (\de -> delta (f x) de) (monad-law-4-1 (S O) f ds) ⟩
321 delta (f x) (delta-fmap f (delta-bind ds tailDelta)) ≡⟨ refl ⟩
322 delta-fmap f (delta x (delta-bind ds tailDelta)) ≡⟨ refl ⟩
323 delta-fmap f (delta (headDelta (delta x d)) (delta-bind ds tailDelta)) ≡⟨ refl ⟩
324 delta-fmap f (delta-mu (delta (delta x d) ds)) ≡⟨ refl ⟩
325 (delta-fmap f ∙ delta-mu) (delta (delta x d) ds) ∎
326
327 -}
328 -- monad-law-1 : join . delta-fmap join = join . join
329 monad-law-1 : {l : Level} {A : Set l} {a : Rev} -> (d : Delta (Delta (Delta A a) a) a) ->
330 ((delta-mu ∙ (delta-fmap delta-mu)) d) ≡ ((delta-mu ∙ delta-mu) d)
331 monad-law-1 (mono d) = refl
332 monad-law-1 (delta d ds) = {!!}
333
334 delta-is-monad : {l : Level} {v : Rev} -> Monad {l} (\A -> Delta A v) delta-is-functor
335 128
336 129
337 delta-is-monad = record { eta = delta-eta; 130 delta-is-monad = record { eta = delta-eta;
338 mu = delta-mu; 131 mu = delta-mu;
339 return = delta-eta; 132 return = delta-eta;
340 bind = delta-bind; 133 bind = delta-bind;
341 association-law = monad-law-1 } 134 eta-is-nt = delta-eta-is-nt;
342 -- left-unity-law = monad-law-2; 135 association-law = monad-law-1;
343 -- right-unity-law = monad-law-2' } 136 left-unity-law = delta-left-unity-law ;
137 right-unity-law = \x -> (sym (delta-right-unity-law x)) }
344 138
345 139
346 140
347 141
348 142
349 {- 143 {-
350 144
351 -- Monad-laws (Haskell) 145 -- Monad-laws (Haskell)
352 -- monad-law-h-1 : return a >>= k = k a 146 -- monad-law-h-1 : return a >>= k = k a
353 monad-law-h-1 : {l : Level} {A B : Set l} -> 147 monad-law-h-1 : {l : Level} {A B : Set l} ->
354 (a : A) -> (k : A -> (Delta B)) -> 148 (a : A) -> (k : A -> (Delta B)) ->
355 (delta-return a >>= k) ≡ (k a) 149 (delta-return a >>= k) ≡ (k a)
356 monad-law-h-1 a k = refl 150 monad-law-h-1 a k = refl
357 151
358 152
363 monad-law-h-2 (delta x d) = cong (delta x) (monad-law-h-2 d) 157 monad-law-h-2 (delta x d) = cong (delta x) (monad-law-h-2 d)
364 158
365 159
366 160
367 -- monad-law-h-3 : m >>= (\x -> f x >>= g) = (m >>= f) >>= g 161 -- monad-law-h-3 : m >>= (\x -> f x >>= g) = (m >>= f) >>= g
368 monad-law-h-3 : {l : Level} {A B C : Set l} -> 162 monad-law-h-3 : {l : Level} {A B C : Set l} ->
369 (m : Delta A) -> (f : A -> (Delta B)) -> (g : B -> (Delta C)) -> 163 (m : Delta A) -> (f : A -> (Delta B)) -> (g : B -> (Delta C)) ->
370 (delta-bind m (\x -> delta-bind (f x) g)) ≡ (delta-bind (delta-bind m f) g) 164 (delta-bind m (\x -> delta-bind (f x) g)) ≡ (delta-bind (delta-bind m f) g)
371 monad-law-h-3 (mono x) f g = refl 165 monad-law-h-3 (mono x) f g = refl
372 monad-law-h-3 (delta x d) f g = begin 166 monad-law-h-3 (delta x d) f g = begin
373 (delta-bind (delta x d) (\x -> delta-bind (f x) g)) ≡⟨ {!!} ⟩ 167 (delta-bind (delta x d) (\x -> delta-bind (f x) g)) ≡⟨ {!!} ⟩