Mercurial > hg > Members > atton > delta_monad
annotate agda/deltaM/monad.agda @ 98:b7f0879e854e
Trying Monad-laws for DeltaM
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 21 Jan 2015 17:43:53 +0900 |
parents | |
children | 9c62373bd474 |
rev | line source |
---|---|
98
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 open import Level |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 open import Relation.Binary.PropositionalEquality |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 open ≡-Reasoning |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 open import basic |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 open import delta |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 open import delta.functor |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 open import deltaM |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 open import deltaM.functor |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 open import laws |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 module deltaM.monad where |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 open Functor |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 open NaturalTransformation |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 open Monad |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 postulate deltaM-mu-is-natural-transformation : {l : Level} {A : Set l} |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 {M : {l' : Level} -> Set l' -> Set l'} -> |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 {functorM : {l' : Level} -> Functor {l'} M} |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M (functorM ) } -> |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 NaturalTransformation (\A -> DeltaM M (DeltaM M A)) (\A -> DeltaM M A) |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 {deltaM-fmap ∙ deltaM-fmap} {deltaM-fmap {l}} |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 (deltaM-mu {_} {_} {M} {functorM} {monadM}) |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 headDeltaM-commute : {l : Level} {A B : Set l} |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 {M : {l' : Level} -> Set l' -> Set l'} -> |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 {functorM : {l' : Level} -> Functor {l'} M} -> |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M (functorM ) } -> |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 (f : A -> B) -> (x : DeltaM M {functorM} {monadM} A) -> |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 headDeltaM (deltaM-fmap f x) ≡ fmap functorM f (headDeltaM x) |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 headDeltaM-commute f (deltaM (mono x)) = refl |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 headDeltaM-commute f (deltaM (delta x d)) = refl |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
36 headDeltaM-is-natural-transformation : {l : Level} {A : Set l} |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
37 {M : {l' : Level} -> Set l' -> Set l'} -> |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
38 {functorM : {l' : Level} -> Functor {l'} M} |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM } -> |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
40 NaturalTransformation {l} (\A -> DeltaM M {functorM} {monadM} A) M |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 {\f d → deltaM (mono (headDeltaM (deltaM-fmap f d)))} {fmap functorM} headDeltaM |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 -- {deltaM-fmap} {fmap (functorM {l} {A})} headDeltaM |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 headDeltaM-is-natural-transformation = record { commute = headDeltaM-commute } |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
44 |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
46 |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
47 deltaM-association-law : {l : Level} {A : Set l} |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
48 {M : {l' : Level} -> Set l' -> Set l'} |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
49 (functorM : {l' : Level} -> Functor {l'} M) |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
50 (monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM) |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
51 -> (d : DeltaM M (DeltaM M (DeltaM M {functorM} {monadM} A))) |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
52 -> ((deltaM-mu ∙ (deltaM-fmap deltaM-mu)) d) ≡ ((deltaM-mu ∙ deltaM-mu) d) |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
53 deltaM-association-law functorM monadM (deltaM x) = {!!} |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
54 {- |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
55 begin |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
56 (deltaM-mu ∙ deltaM-fmap deltaM-mu) d ≡⟨ refl ⟩ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
57 deltaM-mu (deltaM-fmap deltaM-mu d) ≡⟨ {!!} ⟩ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
58 deltaM-mu (deltaM-mu d) ≡⟨ refl ⟩ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
59 (deltaM-mu ∙ deltaM-mu) d |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
60 ∎ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
61 -} |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
62 {- |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
63 deltaM-association-law functorM monadM (deltaM (mono x)) = begin |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
64 (deltaM-mu ∙ deltaM-fmap deltaM-mu) (deltaM (mono x)) ≡⟨ refl ⟩ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
65 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
66 deltaM-mu (deltaM (delta-fmap (fmap functorM deltaM-mu) (mono x))) ≡⟨ refl ⟩ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
67 deltaM-mu (deltaM (mono (fmap functorM deltaM-mu x))) ≡⟨ refl ⟩ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
68 deltaM-bind (deltaM (mono (fmap functorM deltaM-mu x))) id ≡⟨ refl ⟩ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
69 deltaM (mono (bind monadM (fmap functorM deltaM-mu x) (headDeltaM ∙ id))) ≡⟨ refl ⟩ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
70 deltaM (mono (bind monadM (fmap functorM deltaM-mu x) headDeltaM)) ≡⟨ {!!} ⟩ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
71 deltaM (mono (bind monadM (bind monadM x headDeltaM) headDeltaM)) ≡⟨ refl ⟩ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
72 deltaM (mono (bind monadM (bind monadM x (headDeltaM ∙ id)) (headDeltaM ∙ id))) ≡⟨ refl ⟩ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
73 deltaM-mu (deltaM (mono (bind monadM x (headDeltaM ∙ id)))) ≡⟨ refl ⟩ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
74 deltaM-mu (deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
75 (deltaM-mu ∙ deltaM-mu) (deltaM (mono x)) ∎ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
76 deltaM-association-law functorM monadM (deltaM (delta x d)) = {!!} |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
77 -} |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
78 |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
79 {- |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
80 |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
81 nya : {l : Level} {A B C : Set l} -> |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
82 {M : {l' : Level} -> Set l' -> Set l'} |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
83 {functorM : {l' : Level} -> Functor {l'} M } |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
84 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
85 (m : DeltaM M {functorM} {monadM} A) -> (f : A -> (DeltaM M {functorM} {monadM} B)) -> (g : B -> (DeltaM M C)) -> |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
86 (x : M A) -> |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
87 (deltaM (fmap delta-is-functor (\x -> bind {l} {A} monadM x (headDeltaM ∙ (\x -> deltaM-bind (f x) g))) (mono x))) ≡ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
88 (deltaM-bind (deltaM (fmap delta-is-functor (\x -> (bind {l} {A} monadM x (headDeltaM ∙ f))) (mono x))) g) |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
89 nya = {!!} |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
90 |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
91 deltaM-monad-law-h-3 : {l : Level} {A B C : Set l} -> |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
92 {M : {l' : Level} -> Set l' -> Set l'} |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
93 {functorM : {l' : Level} -> Functor {l'} M } |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
94 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
95 (m : DeltaM M {functorM} {monadM} A) -> (f : A -> (DeltaM M B)) -> (g : B -> (DeltaM M C)) -> |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
96 (deltaM-bind m (\x -> deltaM-bind (f x) g)) ≡ (deltaM-bind (deltaM-bind m f) g) |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
97 {- |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
98 deltaM-monad-law-h-3 {l} {A} {B} {C} {M} {functorM} {monadM} (deltaM (mono x)) f g = begin |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
99 (deltaM-bind (deltaM (mono x)) (\x -> deltaM-bind (f x) g)) ≡⟨ refl ⟩ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
100 |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
101 (deltaM (mono (bind {l} {A} monadM x (headDeltaM ∙ (\x -> deltaM-bind (f x) g))))) ≡⟨ {!!} ⟩ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
102 (deltaM-bind (deltaM (fmap delta-is-functor (\x -> (bind {l} {A} monadM x (headDeltaM ∙ f))) (mono x))) g) ≡⟨ refl ⟩ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
103 (deltaM-bind (deltaM (mono (bind {l} {A} monadM x (headDeltaM ∙ f)))) g) ≡⟨ refl ⟩ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
104 (deltaM-bind (deltaM-bind (deltaM (mono x)) f) g) ∎ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
105 -} |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
106 |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
107 deltaM-monad-law-h-3 {l} {A} {B} {C} {M} {functorM} {monadM} (deltaM (mono x)) f g = begin |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
108 (deltaM-bind (deltaM (mono x)) (\x -> deltaM-bind (f x) g)) ≡⟨ refl ⟩ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
109 (deltaM (mono (bind {l} {A} monadM x (headDeltaM ∙ (\x -> deltaM-bind (f x) g))))) ≡⟨ {!!} ⟩ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
110 -- (deltaM (fmap delta-is-functor (\x -> bind {l} {A} monadM x (headDeltaM ∙ (\x -> deltaM-bind (f x) g))) (mono x))) ≡⟨ {!!} ⟩ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
111 deltaM (mono (bind {l} {B} monadM (bind {_} {A} monadM x (headDeltaM ∙ f)) (headDeltaM ∙ g))) ≡⟨ {!!} ⟩ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
112 deltaM (mono (bind {l} {B} monadM (bind {_} {A} monadM x (headDeltaM ∙ f)) (headDeltaM ∙ g))) ≡⟨ {!!} ⟩ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
113 (deltaM-bind (deltaM (mono (bind {l} {A} monadM x (headDeltaM ∙ f)))) g) ≡⟨ refl ⟩ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
114 (deltaM-bind (deltaM-bind (deltaM (mono x)) f) g) |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
115 ∎ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
116 deltaM-monad-law-h-3 (deltaM (delta x d)) f g = {!!} |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
117 {- |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
118 begin |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
119 (deltaM-bind m (\x -> deltaM-bind (f x) g)) ≡⟨ {!!} ⟩ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
120 (deltaM-bind (deltaM-bind m f) g) |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
121 ∎ |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
122 -} |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
123 -} |